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  866  nfalt  1558  alexim  1625  19.36-1  1652  ax11ev  1801  equs5or  1803  necon2bd  2367  necon2d  2368  necon1bbiddc  2372  necon2abiddc  2375  necon2bbiddc  2376  necon4idc  2378  necon4ddc  2381  necon1bddc  2386  spc2gv  2780  spc3gv  2782  mo2icl  2867  reupick  3365  prneimg  3709  invdisj  3931  trin  4044  exmidsssnc  4134  ordsucss  4428  eqbrrdva  4717  elreldm  4773  elres  4863  xp11m  4985  ssrnres  4989  opelf  5302  dffo4  5576  dftpos3  6167  tfr1onlemaccex  6253  tfrcllemaccex  6266  nnaordex  6431  swoer  6465  map0g  6590  mapsn  6592  nneneq  6759  fnfi  6833  prarloclemlo  7326  genprndl  7353  genprndu  7354  cauappcvgprlemladdrl  7489  caucvgprlemladdrl  7510  caucvgsrlemoffres  7632  caucvgsr  7634  nntopi  7726  letr  7871  reapcotr  8384  apcotr  8393  mulext1  8398  cnstab  8431  lt2msq  8668  nneoor  9177  xrletr  9621  icoshft  9803  caucvgre  10785  absext  10867  rexico  11025  summodc  11184  gcdeq0  11701  tgcn  12416  cnptoprest  12447  metequiv2  12704  bj-nnsn  13116  bj-inf2vnlem2  13340