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  1592  alexim  1659  19.36-1  1687  ax11ev  1842  equs5or  1844  necon2bd  2425  necon2d  2426  necon1bbiddc  2430  necon2abiddc  2433  necon2bbiddc  2434  necon4idc  2436  necon4ddc  2439  necon1bddc  2444  spc2gv  2855  spc3gv  2857  mo2icl  2943  reupick  3448  prneimg  3805  invdisj  4028  trin  4142  exmidsssnc  4237  ordsucss  4541  eqbrrdva  4837  elreldm  4893  elres  4983  xp11m  5109  ssrnres  5113  opelf  5432  dffo4  5713  dftpos3  6329  tfr1onlemaccex  6415  tfrcllemaccex  6428  nnaordex  6595  swoer  6629  map0g  6756  mapsn  6758  nneneq  6927  fnfi  7011  prarloclemlo  7578  genprndl  7605  genprndu  7606  cauappcvgprlemladdrl  7741  caucvgprlemladdrl  7762  caucvgsrlemoffres  7884  caucvgsr  7886  nntopi  7978  letr  8126  reapcotr  8642  apcotr  8651  mulext1  8656  lt2msq  8930  nneoor  9445  xrletr  9900  icoshft  10082  caucvgre  11163  absext  11245  rexico  11403  summodc  11565  gcdeq0  12169  intopsn  13069  znleval  14285  tgcn  14528  cnptoprest  14559  metequiv2  14816  bj-nnsn  15463  bj-inf2vnlem2  15701