Theorem sylan2b 285

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	|- ( ph <-> ch )
sylan2b.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan2b	|- ( ( ps /\ ph ) -> th )

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 |- ( ph <-> ch )
2	1	biimpi 119	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 284	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  289  dcor  920  bm1.1  2142  eqtr3  2177  elnelne1  2431  elnelne2  2432  morex  2896  reuss2  3387  reupick  3391  rabsneu  3632  opabss  4028  triun  4075  poirr  4267  wepo  4319  wetrep  4320  rexxfrd  4422  reg3exmidlemwe  4537  nnsuc  4574  fnfco  5343  fun11iun  5434  fnressn  5652  fvpr1g  5672  fvtp1g  5674  fvtp3g  5676  fvtp3  5679  f1mpt  5718  caovlem2d  6010  offval  6036  dfoprab3  6136  1stconst  6165  2ndconst  6166  poxp  6176  tfrlemisucaccv  6269  tfr1onlemsucaccv  6285  tfrcllemsucaccv  6298  fiintim  6870  addclpi  7241  addnidpig  7250  reapmul1  8464  nnnn0addcl  9114  un0addcl  9117  un0mulcl  9118  zltnle  9207  nn0ge0div  9245  uzind3  9271  uzind4  9493  ltsubrp  9590  ltaddrp  9591  xrlttr  9695  xrltso  9696  xltnegi  9732  xaddnemnf  9754  xaddnepnf  9755  xaddcom  9758  xnegdi  9765  xsubge0  9778  fzind2  10131  qltnle  10138  qbtwnxr  10150  exp3vallem  10413  expp1  10419  expnegap0  10420  expcllem  10423  mulexpzap  10452  expaddzap  10456  expmulzap  10458  hashunlem  10671  shftf  10723  sqrtdiv  10935  mulcn2  11202  summodclem2  11272  fsum3  11277  cvgratz  11422  prodmodclem2  11467  zproddc  11469  prodsnf  11482  dvdsflip  11735  dvdsfac  11744  lcmgcdlem  11945  rpexp1i  12019  hashdvds  12084  hashgcdlem  12101  phisum  12103  lmss  12617  xmetrtri  12747  blssioo  12916  divcnap  12926  dedekindicc  12982  dvidlemap  13031  dvrecap  13048  dveflem  13058  bj-bdfindes  13495  bj-findes  13527