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  1588  alexim  1655  19.36-1  1683  ax11ev  1838  equs5or  1840  necon2bd  2415  necon2d  2416  necon1bbiddc  2420  necon2abiddc  2423  necon2bbiddc  2424  necon4idc  2426  necon4ddc  2429  necon1bddc  2434  spc2gv  2840  spc3gv  2842  mo2icl  2928  reupick  3431  prneimg  3786  invdisj  4009  trin  4123  exmidsssnc  4215  ordsucss  4515  eqbrrdva  4809  elreldm  4865  elres  4955  xp11m  5079  ssrnres  5083  opelf  5399  dffo4  5677  dftpos3  6277  tfr1onlemaccex  6363  tfrcllemaccex  6376  nnaordex  6543  swoer  6577  map0g  6702  mapsn  6704  nneneq  6871  fnfi  6950  prarloclemlo  7507  genprndl  7534  genprndu  7535  cauappcvgprlemladdrl  7670  caucvgprlemladdrl  7691  caucvgsrlemoffres  7813  caucvgsr  7815  nntopi  7907  letr  8054  reapcotr  8569  apcotr  8578  mulext1  8583  lt2msq  8857  nneoor  9369  xrletr  9822  icoshft  10004  caucvgre  11004  absext  11086  rexico  11244  summodc  11405  gcdeq0  11992  intopsn  12805  tgcn  14061  cnptoprest  14092  metequiv2  14349  bj-nnsn  14838  bj-inf2vnlem2  15076