Theorem syl6ib 150

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl6ib.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl6ib.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
syl6ib	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6ib.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	biimpi 113	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 29	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr3g  193  exp4a  348  con2biddc  774  nfalt  1470  alexim  1536  19.36-1  1563  ax11ev  1709  equs5or  1711  necon2bd  2263  necon2d  2264  necon1bbiddc  2268  necon2abiddc  2271  necon2bbiddc  2272  necon4idc  2274  necon4ddc  2277  necon1bddc  2282  spc2gv  2643  spc3gv  2645  mo2icl  2720  eqsbc3r  2819  reupick  3221  prneimg  3545  invdisj  3759  trin  3864  ordsucss  4230  eqbrrdva  4505  elreldm  4560  elres  4646  xp11m  4759  ssrnres  4763  opelf  5062  dffo4  5315  dftpos3  5877  tfr0  5937  nnaordex  6100  swoer  6134  nneneq  6320  prarloclemlo  6592  genprndl  6619  genprndu  6620  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  caucvgsrlemoffres  6884  caucvgsr  6886  nntopi  6968  letr  7101  reapcotr  7589  apcotr  7598  mulext1  7603  lt2msq  7852  nneoor  8340  xrletr  8724  icoshft  8858  caucvgre  9580  absext  9661  bj-inf2vnlem2  10096