Theorem syl6ib 160

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 119	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 33	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3g  203  exp4a  361  con2biddc  848  nfalt  1540  alexim  1607  19.36-1  1634  ax11ev  1782  equs5or  1784  necon2bd  2340  necon2d  2341  necon1bbiddc  2345  necon2abiddc  2348  necon2bbiddc  2349  necon4idc  2351  necon4ddc  2354  necon1bddc  2359  spc2gv  2747  spc3gv  2749  mo2icl  2832  reupick  3326  prneimg  3667  invdisj  3889  trin  3996  exmidsssnc  4086  ordsucss  4380  eqbrrdva  4669  elreldm  4725  elres  4813  xp11m  4935  ssrnres  4939  opelf  5252  dffo4  5522  dftpos3  6113  tfr1onlemaccex  6199  tfrcllemaccex  6212  nnaordex  6377  swoer  6411  map0g  6536  mapsn  6538  nneneq  6704  fnfi  6777  prarloclemlo  7250  genprndl  7277  genprndu  7278  cauappcvgprlemladdrl  7413  caucvgprlemladdrl  7434  caucvgsrlemoffres  7542  caucvgsr  7544  nntopi  7629  letr  7770  reapcotr  8278  apcotr  8287  mulext1  8292  cnstab  8324  lt2msq  8554  nneoor  9057  xrletr  9484  icoshft  9666  caucvgre  10645  absext  10727  rexico  10885  summodc  11044  gcdeq0  11513  tgcn  12219  cnptoprest  12250  metequiv2  12485  bj-nnsn  12638  bj-inf2vnlem2  12861