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  6428  tfr1onlemaccex  6514  tfrcllemaccex  6527  nnaordex  6696  swoer  6730  map0g  6857  mapsn  6859  nneneq  7043  fnfi  7135  prarloclemlo  7714  genprndl  7741  genprndu  7742  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgsrlemoffres  8020  caucvgsr  8022  nntopi  8114  letr  8262  reapcotr  8778  apcotr  8787  mulext1  8792  lt2msq  9066  nneoor  9582  xrletr  10043  icoshft  10225  swrdccatin2  11314  caucvgre  11559  absext  11641  rexico  11799  summodc  11962  gcdeq0  12566  intopsn  13468  znleval  14686  tgcn  14951  cnptoprest  14982  metequiv2  15239  bj-nnsn  16380  bj-inf2vnlem2  16617