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  875  nfalt  1571  alexim  1638  19.36-1  1666  ax11ev  1821  equs5or  1823  necon2bd  2398  necon2d  2399  necon1bbiddc  2403  necon2abiddc  2406  necon2bbiddc  2407  necon4idc  2409  necon4ddc  2412  necon1bddc  2417  spc2gv  2821  spc3gv  2823  mo2icl  2909  reupick  3411  prneimg  3761  invdisj  3983  trin  4097  exmidsssnc  4189  ordsucss  4488  eqbrrdva  4781  elreldm  4837  elres  4927  xp11m  5049  ssrnres  5053  opelf  5369  dffo4  5644  dftpos3  6241  tfr1onlemaccex  6327  tfrcllemaccex  6340  nnaordex  6507  swoer  6541  map0g  6666  mapsn  6668  nneneq  6835  fnfi  6914  prarloclemlo  7456  genprndl  7483  genprndu  7484  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  caucvgsrlemoffres  7762  caucvgsr  7764  nntopi  7856  letr  8002  reapcotr  8517  apcotr  8526  mulext1  8531  lt2msq  8802  nneoor  9314  xrletr  9765  icoshft  9947  caucvgre  10945  absext  11027  rexico  11185  summodc  11346  gcdeq0  11932  intopsn  12621  tgcn  13002  cnptoprest  13033  metequiv2  13290  bj-nnsn  13768  bj-inf2vnlem2  14006