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  887  nfalt  1626  alexim  1693  19.36-1  1721  ax11ev  1876  equs5or  1878  necon2bd  2460  necon2d  2461  necon1bbiddc  2465  necon2abiddc  2468  necon2bbiddc  2469  necon4idc  2471  necon4ddc  2474  necon1bddc  2479  spc2gv  2897  spc3gv  2899  mo2icl  2985  reupick  3491  prneimg  3857  invdisj  4081  trin  4197  exmidsssnc  4293  ordsucss  4602  eqbrrdva  4900  elreldm  4958  elres  5049  xp11m  5175  ssrnres  5179  opelf  5507  dffo4  5795  dftpos3  6427  tfr1onlemaccex  6513  tfrcllemaccex  6526  nnaordex  6695  swoer  6729  map0g  6856  mapsn  6858  nneneq  7042  fnfi  7134  prarloclemlo  7713  genprndl  7740  genprndu  7741  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  caucvgsrlemoffres  8019  caucvgsr  8021  nntopi  8113  letr  8261  reapcotr  8777  apcotr  8786  mulext1  8791  lt2msq  9065  nneoor  9581  xrletr  10042  icoshft  10224  swrdccatin2  11309  caucvgre  11541  absext  11623  rexico  11781  summodc  11943  gcdeq0  12547  intopsn  13449  znleval  14666  tgcn  14931  cnptoprest  14962  metequiv2  15219  bj-nnsn  16329  bj-inf2vnlem2  16566