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  2894  spc3gv  2896  mo2icl  2982  reupick  3488  prneimg  3851  invdisj  4075  trin  4191  exmidsssnc  4286  ordsucss  4595  eqbrrdva  4891  elreldm  4949  elres  5040  xp11m  5166  ssrnres  5170  opelf  5495  dffo4  5782  dftpos3  6406  tfr1onlemaccex  6492  tfrcllemaccex  6505  nnaordex  6672  swoer  6706  map0g  6833  mapsn  6835  nneneq  7014  fnfi  7099  prarloclemlo  7677  genprndl  7704  genprndu  7705  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  caucvgsrlemoffres  7983  caucvgsr  7985  nntopi  8077  letr  8225  reapcotr  8741  apcotr  8750  mulext1  8755  lt2msq  9029  nneoor  9545  xrletr  10000  icoshft  10182  swrdccatin2  11256  caucvgre  11487  absext  11569  rexico  11727  summodc  11889  gcdeq0  12493  intopsn  13395  znleval  14611  tgcn  14876  cnptoprest  14907  metequiv2  15164  bj-nnsn  16055  bj-inf2vnlem2  16292