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-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3g  203  exp4a  363  con2biddc  865  nfalt  1557  alexim  1624  19.36-1  1651  ax11ev  1800  equs5or  1802  necon2bd  2366  necon2d  2367  necon1bbiddc  2371  necon2abiddc  2374  necon2bbiddc  2375  necon4idc  2377  necon4ddc  2380  necon1bddc  2385  spc2gv  2776  spc3gv  2778  mo2icl  2863  reupick  3360  prneimg  3701  invdisj  3923  trin  4036  exmidsssnc  4126  ordsucss  4420  eqbrrdva  4709  elreldm  4765  elres  4855  xp11m  4977  ssrnres  4981  opelf  5294  dffo4  5568  dftpos3  6159  tfr1onlemaccex  6245  tfrcllemaccex  6258  nnaordex  6423  swoer  6457  map0g  6582  mapsn  6584  nneneq  6751  fnfi  6825  prarloclemlo  7302  genprndl  7329  genprndu  7330  cauappcvgprlemladdrl  7465  caucvgprlemladdrl  7486  caucvgsrlemoffres  7608  caucvgsr  7610  nntopi  7702  letr  7847  reapcotr  8360  apcotr  8369  mulext1  8374  cnstab  8407  lt2msq  8644  nneoor  9153  xrletr  9591  icoshft  9773  caucvgre  10753  absext  10835  rexico  10993  summodc  11152  gcdeq0  11665  tgcn  12377  cnptoprest  12408  metequiv2  12665  bj-nnsn  12945  bj-inf2vnlem2  13169