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  885  nfalt  1624  alexim  1691  19.36-1  1719  ax11ev  1874  equs5or  1876  necon2bd  2458  necon2d  2459  necon1bbiddc  2463  necon2abiddc  2466  necon2bbiddc  2467  necon4idc  2469  necon4ddc  2472  necon1bddc  2477  spc2gv  2894  spc3gv  2896  mo2icl  2982  reupick  3488  prneimg  3852  invdisj  4076  trin  4192  exmidsssnc  4287  ordsucss  4596  eqbrrdva  4892  elreldm  4950  elres  5041  xp11m  5167  ssrnres  5171  opelf  5498  dffo4  5785  dftpos3  6414  tfr1onlemaccex  6500  tfrcllemaccex  6513  nnaordex  6682  swoer  6716  map0g  6843  mapsn  6845  nneneq  7026  fnfi  7114  prarloclemlo  7692  genprndl  7719  genprndu  7720  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  caucvgsrlemoffres  7998  caucvgsr  8000  nntopi  8092  letr  8240  reapcotr  8756  apcotr  8765  mulext1  8770  lt2msq  9044  nneoor  9560  xrletr  10016  icoshft  10198  swrdccatin2  11276  caucvgre  11507  absext  11589  rexico  11747  summodc  11909  gcdeq0  12513  intopsn  13415  znleval  14632  tgcn  14897  cnptoprest  14928  metequiv2  15185  bj-nnsn  16152  bj-inf2vnlem2  16389