Theorem sylan2b 287

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 120	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 286	1 |- ( ( ps /\ ph ) -> th )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl2anb  291  dcor  935  bm1.1  2162  eqtr3  2197  elnelne1  2451  elnelne2  2452  morex  2923  reuss2  3417  reupick  3421  rabsneu  3667  opabss  4069  triun  4116  poirr  4309  wepo  4361  wetrep  4362  rexxfrd  4465  reg3exmidlemwe  4580  nnsuc  4617  fnfco  5392  fun11iun  5484  fnressn  5704  fvpr1g  5724  fvtp1g  5726  fvtp3g  5728  fvtp3  5731  f1mpt  5774  caovlem2d  6069  offval  6092  dfoprab3  6194  1stconst  6224  2ndconst  6225  poxp  6235  tfrlemisucaccv  6328  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  fiintim  6930  addclpi  7328  addnidpig  7337  reapmul1  8554  nnnn0addcl  9208  un0addcl  9211  un0mulcl  9212  zltnle  9301  nn0ge0div  9342  uzind3  9368  uzind4  9590  ltsubrp  9692  ltaddrp  9693  xrlttr  9797  xrltso  9798  xltnegi  9837  xaddnemnf  9859  xaddnepnf  9860  xaddcom  9863  xnegdi  9870  xsubge0  9883  fzind2  10241  qltnle  10248  qbtwnxr  10260  exp3vallem  10523  expp1  10529  expnegap0  10530  expcllem  10533  mulexpzap  10562  expaddzap  10566  expmulzap  10568  hashunlem  10786  shftf  10841  sqrtdiv  11053  mulcn2  11322  summodclem2  11392  fsum3  11397  cvgratz  11542  prodmodclem2  11587  zproddc  11589  prodsnf  11602  dvdsflip  11859  dvdsfac  11868  lcmgcdlem  12079  rpexp1i  12156  hashdvds  12223  hashgcdlem  12240  phisum  12242  pcqcl  12308  pcid  12325  ssnnctlemct  12449  issubmd  12870  grpinvnzcl  12947  mulgneg  13006  mulgnn0z  13015  01eq0ring  13335  lmss  13785  xmetrtri  13915  blssioo  14084  divcnap  14094  dedekindicc  14150  dvidlemap  14199  dvrecap  14216  dveflem  14226  lgsval3  14458  lgsdir2  14473  2sqlem6  14506  bj-bdfindes  14740  bj-findes  14772