Theorem sylan2 270

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

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

Assertion

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

Proof of Theorem sylan2

Step	Hyp	Ref	Expression
1		sylan2.1	. . 3 |- ( ph -> ch )
2	1	adantl 262	. 2 |- ( ( ps /\ ph ) -> ch )
3		sylan2.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	syldan 266	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  sylan2b  271  sylan2br  272  syl2an  273  sylanr1  384  sylanr2  385  mpanr2  414  adantrl  447  adantrr  448  ancom2s  500  3adantr1  1063  3adantr2  1064  3adantr3  1065  syl3anr1  1187  syl3anr3  1189  dfbi3dc  1288  xordidc  1290  elabgt  2684  sbciegft  2793  csbtt  2862  csbnestgf  2898  copsex2t  3982  pofun  4049  onsucmin  4233  onsucelsucr  4234  onsucsssucr  4235  ordsucunielexmid  4256  ordsuc  4287  nlimsucg  4290  elnn  4328  xpsspw  4450  elxp4  4808  elxp5  4809  funimass2  4977  imain  4981  funimaexg  4983  dff1o2  5131  resdif  5148  funbrfv  5212  fvelimab  5229  eqfnfv2  5266  fvimacnvi  5281  ffvresb  5328  fnressn  5349  fmptapd  5354  fnex  5383  rexima  5394  ralima  5395  f1elima  5412  fnotovb  5548  mpt2eq12  5565  fovrn  5643  fnovrn  5648  ofrfval  5720  fnofval  5721  cofunexg  5738  cofunex2g  5739  mpt2exxg  5833  mpt2exg  5834  f1o2ndf1  5849  smodm2  5910  tfrlem9  5935  tfrlemibxssdm  5941  tfri3  5953  rdgtfr  5961  rdgruledefgg  5962  frecsuclem1  5987  oav2  6043  oasuc  6044  omv2  6045  onasuc  6046  omsuc  6051  onmsuc  6052  nnaass  6064  nndi  6065  nndir  6069  nnaword  6084  ecelqsg  6159  iinerm  6178  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  domentr  6271  xpdom1g  6307  fopwdom  6310  phplem3  6317  phplem4  6318  php5dom  6325  ssfiexmid  6336  diffitest  6344  addclpi  6425  addasspig  6428  mulasspig  6430  distrpig  6431  mulcanpig  6433  nnppipi  6441  enqdc1  6460  addassnqg  6480  ltbtwnnqq  6513  prarloclemarch  6516  prarloclemarch2  6517  enq0sym  6530  enq0ref  6531  addclnq0  6549  nqpnq0nq  6551  nnanq0  6556  distrnq0  6557  addassnq0lemcl  6559  addassnq0  6560  distnq0r  6561  prarloclemlt  6591  genpassl  6622  genpassu  6623  genpassg  6624  nqpru  6650  addcomprg  6676  mulcomprg  6678  distrlem1prl  6680  distrlem1pru  6681  1idprl  6688  1idpru  6689  recexprlemdisj  6728  recexprlem1ssl  6731  peano2nnnn  6929  ax1rid  6951  axcaucvglemcl  6969  le2tri3i  7126  add4  7172  cnegexlem1  7186  cnegexlem3  7188  cnegex  7189  subadd  7214  addsub  7222  addsubeq4  7226  negdi  7268  renegcl  7272  resubcl  7275  subdi  7382  mulneg2  7393  mul2neg  7395  submul2  7396  ltnegcon2  7459  lenegcon2  7462  lesub0  7474  cru  7593  recextlem1  7632  recexap  7634  div12ap  7673  divnegap  7683  letrp1  7814  peano2nn  7926  nndivre  7949  nnsub  7952  nndivtr  7955  arch  8178  bndndx  8180  nn0addge1  8228  nn0addge2  8229  zaddcl  8285  zsubcl  8286  zltnle  8291  zrevaddcl  8295  zleltp1  8299  zltlem1  8301  zdiv  8328  peano2uz2  8345  uzind  8349  eluzp1l  8497  ublbneg  8548  qaddcl  8570  qsubcl  8573  qreccl  8576  qdivcl  8577  qrevaddcl  8578  irradd  8580  irrmul  8581  rerpdivcl  8613  xrre  8733  elioc2  8805  icoshft  8858  iccdil  8866  fzss2  8927  fzsuc2  8941  fzrev2  8947  elfzm11  8953  elfzp1b  8959  fzrevral  8967  fzshftral  8970  fzof  9001  fzoval  9005  fzon  9022  fzosubel  9050  zpnn0elfzo  9063  elfzom1b  9085  qltnle  9101  flqlt  9125  flqbi  9132  flqaddz  9139  fzofig  9208  iseqfeq2  9229  iseqfeq  9231  iseqsplit  9238  expp1  9262  expm1t  9283  expeq0  9286  binom2sub  9364  bernneq  9369  expnlbnd  9373  2shfti  9432  crim  9458  mulreap  9464  resub  9470  imsub  9478  ipcnval  9486  cjsub  9492  resqrexlemfp1  9607  resqrexlemgt0  9618  sqabsadd  9653  sqabssub  9654  abs2dif2  9703  cau3lem  9710  icodiamlt  9776  clim  9802  clim2  9804  clim2c  9805  clim0c  9807  2clim  9822  climabs0  9828  climcn1  9829  climcn2  9830  climsqz  9855  climsqz2  9856  climub  9864  climserile  9865  bj-inex  10027  peano5set  10064  findset  10070  bj-findis  10104