Theorem syl6ib 160

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl6ib.1	|- ( ph -> ( ps -> ch ) )
syl6ib.2	|- ( ch <-> th )

Assertion

Ref	Expression
syl6ib	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl6ib.2	. . 3 |- ( ch <-> th )
3	2	biimpi 119	. 2 |- ( ch -> th )
4	1, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3g  203  exp4a  364  con2biddc  870  nfalt  1566  alexim  1633  19.36-1  1661  ax11ev  1816  equs5or  1818  necon2bd  2394  necon2d  2395  necon1bbiddc  2399  necon2abiddc  2402  necon2bbiddc  2403  necon4idc  2405  necon4ddc  2408  necon1bddc  2413  spc2gv  2817  spc3gv  2819  mo2icl  2905  reupick  3406  prneimg  3754  invdisj  3976  trin  4090  exmidsssnc  4182  ordsucss  4481  eqbrrdva  4774  elreldm  4830  elres  4920  xp11m  5042  ssrnres  5046  opelf  5359  dffo4  5633  dftpos3  6230  tfr1onlemaccex  6316  tfrcllemaccex  6329  nnaordex  6495  swoer  6529  map0g  6654  mapsn  6656  nneneq  6823  fnfi  6902  prarloclemlo  7435  genprndl  7462  genprndu  7463  cauappcvgprlemladdrl  7598  caucvgprlemladdrl  7619  caucvgsrlemoffres  7741  caucvgsr  7743  nntopi  7835  letr  7981  reapcotr  8496  apcotr  8505  mulext1  8510  lt2msq  8781  nneoor  9293  xrletr  9744  icoshft  9926  caucvgre  10923  absext  11005  rexico  11163  summodc  11324  gcdeq0  11910  intopsn  12598  tgcn  12848  cnptoprest  12879  metequiv2  13136  bj-nnsn  13614  bj-inf2vnlem2  13853