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  2470  necon2d  2471  necon1bbiddc  2475  necon2abiddc  2478  necon2bbiddc  2479  necon4idc  2481  necon4ddc  2484  necon1bddc  2489  spc2gv  2908  spc3gv  2910  mo2icl  2996  reupick  3505  prneimg  3878  invdisj  4102  trin  4218  exmidsssnc  4316  ordsucss  4626  eqbrrdva  4925  elreldm  4983  elres  5074  xp11m  5201  ssrnres  5205  opelf  5535  dffo4  5825  dftpos3  6493  tfr1onlemaccex  6579  tfrcllemaccex  6592  nnaordex  6761  swoer  6795  map0g  6922  mapsn  6925  nneneq  7111  fnfi  7203  prarloclemlo  7809  genprndl  7836  genprndu  7837  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  caucvgsrlemoffres  8115  caucvgsr  8117  nntopi  8209  letr  8356  reapcotr  8872  apcotr  8881  mulext1  8886  lt2msq  9160  nneoor  9680  xrletr  10141  icoshft  10323  swrdccatin2  11421  caucvgre  11666  absext  11748  rexico  11906  summodc  12069  gcdeq0  12673  intopsn  13580  znleval  14801  tgcn  15073  cnptoprest  15104  metequiv2  15361  bj-nnsn  16505  bj-inf2vnlem2  16741