Theorem syl6ib 161

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

Hypotheses

Ref	Expression
syl6ib.1	|- ( ph -> ( ps -> ch ) )
syl6ib.2	|- ( ch <-> th )

Assertion

Ref	Expression
syl6ib	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl6ib.2	. . 3 |- ( ch <-> th )
3	2	biimpi 120	. 2 |- ( ch -> th )
4	1, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3g  204  exp4a  366  con2biddc  880  nfalt  1578  alexim  1645  19.36-1  1673  ax11ev  1828  equs5or  1830  necon2bd  2405  necon2d  2406  necon1bbiddc  2410  necon2abiddc  2413  necon2bbiddc  2414  necon4idc  2416  necon4ddc  2419  necon1bddc  2424  spc2gv  2828  spc3gv  2830  mo2icl  2916  reupick  3419  prneimg  3773  invdisj  3995  trin  4109  exmidsssnc  4201  ordsucss  4501  eqbrrdva  4794  elreldm  4850  elres  4940  xp11m  5064  ssrnres  5068  opelf  5384  dffo4  5661  dftpos3  6258  tfr1onlemaccex  6344  tfrcllemaccex  6357  nnaordex  6524  swoer  6558  map0g  6683  mapsn  6685  nneneq  6852  fnfi  6931  prarloclemlo  7488  genprndl  7515  genprndu  7516  cauappcvgprlemladdrl  7651  caucvgprlemladdrl  7672  caucvgsrlemoffres  7794  caucvgsr  7796  nntopi  7888  letr  8034  reapcotr  8549  apcotr  8558  mulext1  8563  lt2msq  8837  nneoor  9349  xrletr  9802  icoshft  9984  caucvgre  10981  absext  11063  rexico  11221  summodc  11382  gcdeq0  11968  intopsn  12716  tgcn  13490  cnptoprest  13521  metequiv2  13778  bj-nnsn  14256  bj-inf2vnlem2  14494