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  885  nfalt  1624  alexim  1691  19.36-1  1719  ax11ev  1874  equs5or  1876  necon2bd  2458  necon2d  2459  necon1bbiddc  2463  necon2abiddc  2466  necon2bbiddc  2467  necon4idc  2469  necon4ddc  2472  necon1bddc  2477  spc2gv  2895  spc3gv  2897  mo2icl  2983  reupick  3489  prneimg  3855  invdisj  4079  trin  4195  exmidsssnc  4291  ordsucss  4600  eqbrrdva  4898  elreldm  4956  elres  5047  xp11m  5173  ssrnres  5177  opelf  5504  dffo4  5791  dftpos3  6423  tfr1onlemaccex  6509  tfrcllemaccex  6522  nnaordex  6691  swoer  6725  map0g  6852  mapsn  6854  nneneq  7038  fnfi  7126  prarloclemlo  7704  genprndl  7731  genprndu  7732  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  caucvgsrlemoffres  8010  caucvgsr  8012  nntopi  8104  letr  8252  reapcotr  8768  apcotr  8777  mulext1  8782  lt2msq  9056  nneoor  9572  xrletr  10033  icoshft  10215  swrdccatin2  11300  caucvgre  11532  absext  11614  rexico  11772  summodc  11934  gcdeq0  12538  intopsn  13440  znleval  14657  tgcn  14922  cnptoprest  14953  metequiv2  15210  bj-nnsn  16265  bj-inf2vnlem2  16502