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  1876  equs5or  1878  necon2bd  2461  necon2d  2462  necon1bbiddc  2466  necon2abiddc  2469  necon2bbiddc  2470  necon4idc  2472  necon4ddc  2475  necon1bddc  2480  spc2gv  2898  spc3gv  2900  mo2icl  2986  reupick  3493  prneimg  3862  invdisj  4086  trin  4202  exmidsssnc  4299  ordsucss  4608  eqbrrdva  4906  elreldm  4964  elres  5055  xp11m  5182  ssrnres  5186  opelf  5515  dffo4  5803  dftpos3  6471  tfr1onlemaccex  6557  tfrcllemaccex  6570  nnaordex  6739  swoer  6773  map0g  6900  mapsn  6902  nneneq  7086  fnfi  7178  prarloclemlo  7757  genprndl  7784  genprndu  7785  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  caucvgsrlemoffres  8063  caucvgsr  8065  nntopi  8157  letr  8304  reapcotr  8820  apcotr  8829  mulext1  8834  lt2msq  9108  nneoor  9626  xrletr  10087  icoshft  10269  swrdccatin2  11359  caucvgre  11604  absext  11686  rexico  11844  summodc  12007  gcdeq0  12611  intopsn  13513  znleval  14732  tgcn  15002  cnptoprest  15033  metequiv2  15290  bj-nnsn  16434  bj-inf2vnlem2  16670