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  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  3894  invdisj  4118  trin  4234  exmidsssnc  4335  ordsucss  4646  eqbrrdva  4945  elreldm  5003  elres  5094  xp11m  5221  ssrnres  5225  opelf  5555  dffo4  5847  dftpos3  6523  tfr1onlemaccex  6609  tfrcllemaccex  6622  nnaordex  6791  swoer  6825  map0g  6959  mapsn  6962  nneneq  7148  fnfi  7240  prarloclemlo  7851  genprndl  7878  genprndu  7879  cauappcvgprlemladdrl  8014  caucvgprlemladdrl  8035  caucvgsrlemoffres  8157  caucvgsr  8159  nntopi  8251  letr  8398  reapcotr  8916  apcotr  8925  mulext1  8930  lt2msq  9206  nneoor  9727  xrletr  10189  icoshft  10371  hashf1  11265  swrdccatin2  11479  caucvgre  11725  absext  11807  rexico  11965  summodc  12128  gcdeq0  12732  intopsn  13664  znleval  14960  tgcn  15232  cnptoprest  15263  metequiv2  15520  bj-nnsn  16675  bj-inf2vnlem2  16911