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  882  nfalt  1602  alexim  1669  19.36-1  1697  ax11ev  1852  equs5or  1854  necon2bd  2435  necon2d  2436  necon1bbiddc  2440  necon2abiddc  2443  necon2bbiddc  2444  necon4idc  2446  necon4ddc  2449  necon1bddc  2454  spc2gv  2868  spc3gv  2870  mo2icl  2956  reupick  3461  prneimg  3821  invdisj  4044  trin  4160  exmidsssnc  4255  ordsucss  4560  eqbrrdva  4856  elreldm  4913  elres  5004  xp11m  5130  ssrnres  5134  opelf  5458  dffo4  5741  dftpos3  6361  tfr1onlemaccex  6447  tfrcllemaccex  6460  nnaordex  6627  swoer  6661  map0g  6788  mapsn  6790  nneneq  6969  fnfi  7053  prarloclemlo  7627  genprndl  7654  genprndu  7655  cauappcvgprlemladdrl  7790  caucvgprlemladdrl  7811  caucvgsrlemoffres  7933  caucvgsr  7935  nntopi  8027  letr  8175  reapcotr  8691  apcotr  8700  mulext1  8705  lt2msq  8979  nneoor  9495  xrletr  9950  icoshft  10132  caucvgre  11367  absext  11449  rexico  11607  summodc  11769  gcdeq0  12373  intopsn  13274  znleval  14490  tgcn  14755  cnptoprest  14786  metequiv2  15043  bj-nnsn  15808  bj-inf2vnlem2  16045