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  880  nfalt  1578  alexim  1645  19.36-1  1673  ax11ev  1828  equs5or  1830  necon2bd  2405  necon2d  2406  necon1bbiddc  2410  necon2abiddc  2413  necon2bbiddc  2414  necon4idc  2416  necon4ddc  2419  necon1bddc  2424  spc2gv  2830  spc3gv  2832  mo2icl  2918  reupick  3421  prneimg  3776  invdisj  3999  trin  4113  exmidsssnc  4205  ordsucss  4505  eqbrrdva  4799  elreldm  4855  elres  4945  xp11m  5069  ssrnres  5073  opelf  5389  dffo4  5667  dftpos3  6266  tfr1onlemaccex  6352  tfrcllemaccex  6365  nnaordex  6532  swoer  6566  map0g  6691  mapsn  6693  nneneq  6860  fnfi  6939  prarloclemlo  7496  genprndl  7523  genprndu  7524  cauappcvgprlemladdrl  7659  caucvgprlemladdrl  7680  caucvgsrlemoffres  7802  caucvgsr  7804  nntopi  7896  letr  8043  reapcotr  8558  apcotr  8567  mulext1  8572  lt2msq  8846  nneoor  9358  xrletr  9811  icoshft  9993  caucvgre  10993  absext  11075  rexico  11233  summodc  11394  gcdeq0  11981  intopsn  12793  tgcn  13896  cnptoprest  13927  metequiv2  14184  bj-nnsn  14673  bj-inf2vnlem2  14911