Theorem imbitrdi 161

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

Hypotheses

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

Assertion

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

Proof of Theorem imbitrdi

Step	Hyp	Ref	Expression
1		imbitrdi.1	. 2 |- ( ph -> ( ps -> ch ) )
2		imbitrdi.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  881  nfalt  1600  alexim  1667  19.36-1  1695  ax11ev  1850  equs5or  1852  necon2bd  2433  necon2d  2434  necon1bbiddc  2438  necon2abiddc  2441  necon2bbiddc  2442  necon4idc  2444  necon4ddc  2447  necon1bddc  2452  spc2gv  2863  spc3gv  2865  mo2icl  2951  reupick  3456  prneimg  3814  invdisj  4037  trin  4151  exmidsssnc  4246  ordsucss  4551  eqbrrdva  4847  elreldm  4903  elres  4994  xp11m  5120  ssrnres  5124  opelf  5446  dffo4  5727  dftpos3  6347  tfr1onlemaccex  6433  tfrcllemaccex  6446  nnaordex  6613  swoer  6647  map0g  6774  mapsn  6776  nneneq  6953  fnfi  7037  prarloclemlo  7606  genprndl  7633  genprndu  7634  cauappcvgprlemladdrl  7769  caucvgprlemladdrl  7790  caucvgsrlemoffres  7912  caucvgsr  7914  nntopi  8006  letr  8154  reapcotr  8670  apcotr  8679  mulext1  8684  lt2msq  8958  nneoor  9474  xrletr  9929  icoshft  10111  caucvgre  11234  absext  11316  rexico  11474  summodc  11636  gcdeq0  12240  intopsn  13141  znleval  14357  tgcn  14622  cnptoprest  14653  metequiv2  14910  bj-nnsn  15602  bj-inf2vnlem2  15840