Theorem syl6ib 159

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3g  202  exp4a  358  con2biddc  807  nfalt  1510  alexim  1576  19.36-1  1603  ax11ev  1749  equs5or  1751  necon2bd  2303  necon2d  2304  necon1bbiddc  2308  necon2abiddc  2311  necon2bbiddc  2312  necon4idc  2314  necon4ddc  2317  necon1bddc  2322  spc2gv  2688  spc3gv  2690  mo2icl  2771  reupick  3248  prneimg  3566  invdisj  3780  trin  3885  ordsucss  4248  eqbrrdva  4523  elreldm  4578  elres  4664  xp11m  4779  ssrnres  4783  opelf  5082  dffo4  5336  dftpos3  5900  tfr0  5960  nnaordex  6123  swoer  6157  nneneq  6343  fnfi  6388  prarloclemlo  6684  genprndl  6711  genprndu  6712  cauappcvgprlemladdrl  6847  caucvgprlemladdrl  6868  caucvgsrlemoffres  6976  caucvgsr  6978  nntopi  7060  letr  7194  reapcotr  7698  apcotr  7707  mulext1  7712  lt2msq  7964  nneoor  8449  xrletr  8878  icoshft  9012  caucvgre  9867  absext  9949  rexico  10107  gcdeq0  10368  bj-inf2vnlem2  10766