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  888  nfalt  1627  alexim  1694  19.36-1  1721  ax11ev  1877  equs5or  1879  necon2bd  2472  necon2d  2473  necon1bbiddc  2477  necon2abiddc  2480  necon2bbiddc  2481  necon4idc  2483  necon4ddc  2486  necon1bddc  2491  spc2gv  2910  spc3gv  2912  mo2icl  2999  reupick  3509  prneimg  3883  invdisj  4107  trin  4223  exmidsssnc  4321  ordsucss  4631  eqbrrdva  4930  elreldm  4988  elres  5079  xp11m  5206  ssrnres  5210  opelf  5540  dffo4  5830  dftpos3  6506  tfr1onlemaccex  6592  tfrcllemaccex  6605  nnaordex  6774  swoer  6808  map0g  6935  mapsn  6938  nneneq  7124  fnfi  7216  prarloclemlo  7825  genprndl  7852  genprndu  7853  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgsrlemoffres  8131  caucvgsr  8133  nntopi  8225  letr  8372  reapcotr  8889  apcotr  8898  mulext1  8903  lt2msq  9177  nneoor  9698  xrletr  10160  icoshft  10342  swrdccatin2  11446  caucvgre  11691  absext  11773  rexico  11931  summodc  12094  gcdeq0  12698  intopsn  13630  znleval  14927  tgcn  15199  cnptoprest  15230  metequiv2  15487  bj-nnsn  16631  bj-inf2vnlem2  16867