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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3g  204  exp4a  366  con2biddc  892  nfalt  1631  alexim  1698  19.36-1  1725  ax11ev  1881  equs5or  1883  necon2bd  2478  necon2d  2479  necon1bbiddc  2483  necon2abiddc  2486  necon2bbiddc  2487  necon4idc  2489  necon4ddc  2492  necon1bddc  2497  spc2gv  2916  spc3gv  2918  mo2icl  3005  reupick  3517  prneimg  3899  invdisj  4123  trin  4241  exmidsssnc  4342  ordsucss  4653  eqbrrdva  4952  elreldm  5010  elres  5101  xp11m  5229  ssrnres  5233  opelf  5563  dffo4  5859  dftpos3  6537  tfr1onlemaccex  6623  tfrcllemaccex  6636  nnaordex  6805  swoer  6839  map0g  6973  mapsn  6976  nneneq  7162  fnfi  7254  prarloclemlo  7867  genprndl  7894  genprndu  7895  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgsrlemoffres  8173  caucvgsr  8175  nntopi  8267  letr  8414  reapcotr  8934  apcotr  8943  mulext1  8948  lt2msq  9224  nneoor  9759  xrletr  10227  icoshft  10409  hashf1  11309  swrdccatin2  11523  caucvgre  11769  absext  11851  rexico  12010  summodc  12175  gcdeq0  12779  intopsn  13746  znleval  15097  tgcn  15434  cnptoprest  15465  metequiv2  15722  ppiqeq0  16280  bposlem6  16316  bj-nnsn  16966  bj-inf2vnlem2  17202