Theorem sylbid 178

Description: A syllogism deduction.

Hypotheses

Ref	Expression
sylbid.1	⊢ (φ → (ψ ↔ χ))
sylbid.2	⊢ (φ → (χ → θ))

Assertion

Ref	Expression
sylbid	⊢ (φ → (ψ → θ))

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	biimpd 135	. 2 ⊢ (φ → (ψ → χ))
3		sylbid.2	. 2 ⊢ (φ → (χ → θ))
4	2, 3	syld 27	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 2   ↔ wb 127

This theorem is referenced by:  3imtr4d 421  fvco 2865  isomin 2937  tfrlem5 2953  tfrlem10 2958  tz7.48lem 2993  oevn0 3123  oaass 3163  th3qlem1 3250  dom2d 3307  fundmen 3333  unen 3338  onfin 3415  ssfi 3430  isfinite2 3437  unfilem1 3438  r1tr 3498  r1ord3 3501  bndrank 3526  aceq3 3556  fodom 3613  alephordi 3679  mulcanpi 3821  addnidpi 3822  ltexpq 3874  ltbtwnpq 3878  genpss 3901  genpcd 3903  genpnmax 3904  mulclprlem 3915  distrlem1pr 3921  distrlem4pr 3924  distrlem5pr 3925  ltexprlem3 3938  ltexprlem6 3941  ltexpri 3943  reclem4pr 3953  divadddivt 4264  lelttrt 4289  ltletrt 4290  letrt 4291  elnnz 4572  elnnz1 4581  zltp1let 4597  uzind 4603  indstr 4611  qrecclt 4646  qbtwnre 4650  om2uzf1o 4656  sqr0 4730  sqrlem6 4736  climunii 4883  hlimunii 5143  chocuni 5179  projlem26 5218  h1de2ctlem 5460  spansneleq 5475  spansnsst 5476  spansncv 5542  stadd3 5689  cvcon3t 5716  ssdmd1 5736  atom1d 5750  cvexchlem 5759  atcv0eq 5767  atexch 5769  atcvat4 5775  mdsymlem3 5778  mdsymlem5 5780  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org