Theorem sylan2 284

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 275	. 2 |- ( ( ps /\ ph ) -> ch )
3		sylan2.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	syldan 280	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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 is referenced by:  sylan2b  285  sylan2br  286  syl2an  287  sylanr1  401  sylanr2  402  mpanr2  434  adantrl  469  adantrr  470  ancom2s  555  3adantr1  1140  3adantr2  1141  3adantr3  1142  syl3anr1  1268  syl3anr3  1270  dfbi3dc  1375  xordidc  1377  elabgt  2825  sbciegft  2939  csbtt  3014  csbnestgf  3052  copsex2t  4167  pofun  4234  onsucmin  4423  onsucelsucr  4424  onsucsssucr  4425  ordsucunielexmid  4446  ordsuc  4478  nlimsucg  4481  elnn  4519  xpsspw  4651  elxp4  5026  elxp5  5027  funimass2  5201  imain  5205  funimaexg  5207  f1ff1  5336  dff1o2  5372  resdif  5389  funbrfv  5460  fvelimab  5477  eqfnfv2  5519  fvimacnvi  5534  ffvresb  5583  fnressn  5606  fmptapd  5611  fnex  5642  rexima  5656  ralima  5657  f1elima  5674  fnotovb  5814  mpoeq12  5831  fovrn  5913  fnovrn  5918  ofrfval  5990  ofvalg  5991  cofunexg  6009  cofunex2g  6010  mpoexxg  6108  mpoexg  6109  f1o2ndf1  6125  spc2ed  6130  smodm2  6192  tfrlem9  6216  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  tfri3  6264  rdgtfr  6271  rdgruledefgg  6272  oav2  6359  oasuc  6360  omv2  6361  onasuc  6362  omsuc  6368  onmsuc  6369  nnaass  6381  nndi  6382  nndir  6386  nnaword  6407  ecelqsg  6482  iinerm  6501  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  fvdiagfn  6587  ixpssmap2g  6621  domentr  6685  xpdom1g  6727  fopwdom  6730  ssenen  6745  phplem3  6748  phplem4  6749  php5dom  6757  ssfilem  6769  diffitest  6781  ctssdccl  6996  pm54.43  7046  addclpi  7135  addasspig  7138  mulasspig  7140  distrpig  7141  mulcanpig  7143  nnppipi  7151  enqdc1  7170  addassnqg  7190  ltbtwnnqq  7223  prarloclemarch  7226  prarloclemarch2  7227  enq0sym  7240  enq0ref  7241  addclnq0  7259  nqpnq0nq  7261  nnanq0  7266  distrnq0  7267  addassnq0lemcl  7269  addassnq0  7270  distnq0r  7271  prarloclemlt  7301  genpassl  7332  genpassu  7333  genpassg  7334  nqpru  7360  addcomprg  7386  mulcomprg  7388  distrlem1prl  7390  distrlem1pru  7391  1idprl  7398  1idpru  7399  recexprlemdisj  7438  recexprlem1ssl  7441  peano2nnnn  7661  ax1rid  7685  axcaucvglemcl  7703  le2tri3i  7872  add4  7923  cnegexlem1  7937  cnegexlem3  7939  cnegex  7940  subadd  7965  addsub  7973  addsubeq4  7977  negdi  8019  renegcl  8023  resubcl  8026  subdi  8147  mulneg2  8158  mul2neg  8160  submul2  8161  ltnegcon2  8226  lenegcon2  8229  lesub0  8241  cru  8364  recextlem1  8412  recexap  8414  div12ap  8454  divnegap  8466  letrp1  8606  dfinfre  8714  peano2nn  8732  nndivre  8756  nnsub  8759  nndivtr  8762  arch  8974  bndndx  8976  nn0addge1  9023  nn0addge2  9024  zaddcl  9094  zsubcl  9095  zltnle  9100  zrevaddcl  9104  nzadd  9106  zleltp1  9109  zltlem1  9111  zdiv  9139  peano2uz2  9158  uzind  9162  eluzp1l  9350  ublbneg  9405  qaddcl  9427  qsubcl  9430  qreccl  9434  qdivcl  9435  qrevaddcl  9436  irradd  9438  irrmul  9439  rerpdivcl  9472  nn0ledivnn  9554  xrre  9603  rexsub  9636  xaddass  9652  xnpcan  9655  xsubge0  9664  xposdif  9665  elioc2  9719  icoshft  9773  iccdil  9781  fzss2  9844  fzsuc2  9859  fzrev2  9865  elfzm11  9871  elfzp1b  9877  fzrevral  9885  fzshftral  9888  fzof  9921  fzoval  9925  fzon  9943  fzosubel  9971  zpnn0elfzo  9984  elfzom1b  10006  qltnle  10023  flqlt  10056  flqbi  10063  flqaddz  10070  fzofig  10205  seq3feq2  10243  ser3le  10291  expp1  10300  expm1t  10321  expeq0  10324  binom2sub  10405  bernneq  10412  expnlbnd  10416  faccl  10481  facdiv  10484  bcpasc  10512  bccl  10513  ffz0hash  10576  fnfzo0hash  10578  2shfti  10603  crim  10630  mulreap  10636  resub  10642  imsub  10650  ipcnval  10658  cjsub  10664  resqrexlemfp1  10781  resqrexlemgt0  10792  sqabsadd  10827  sqabssub  10828  abs2dif2  10879  cau3lem  10886  icodiamlt  10952  xrmaxaddlem  11029  clim  11050  clim2  11052  clim2c  11053  clim0c  11055  2clim  11070  climabs0  11076  climcn1  11077  climcn2  11078  climsqz  11104  climsqz2  11105  climub  11113  climserle  11114  fsum3cvg  11147  fisumss  11161  fsum3ser  11166  sumsplitdc  11201  fsump1i  11202  fsumlessfi  11229  telfsumo  11235  fsumparts  11239  iserabs  11244  binomlem  11252  isumsplit  11260  isum1p  11261  isumlessdc  11265  mertenslem2  11305  mertensabs  11306  prodfap0  11314  prodfrecap  11315  prodfdivap  11316  fproddccvg  11341  prodmodclem2  11346  ege2le3  11377  efsub  11387  efexp  11388  efsep  11397  sinsub  11447  cossub  11448  demoivre  11479  eirraplem  11483  moddvds  11502  0dvds  11513  iddvdsexp  11517  dvdssub  11538  dvdsle  11542  dvdsleabs  11543  dvdseq  11546  dvdsflip  11549  mulsucdiv2z  11582  divalgb  11622  divalg2  11623  ndvdsadd  11628  gcdneg  11670  gcdabs2  11678  modgcd  11679  bezoutlemsup  11697  gcdmultiplez  11709  gcdeq  11711  dvdssq  11719  lcmcllem  11748  lcmneg  11755  lcmdvds  11760  qredeu  11778  cncongrcoprm  11787  isprm3  11799  prmrp  11823  divnumden  11874  phiprmpw  11898  crth  11900  hashgcdlem  11903  hashgcdeq  11904  setsresg  11997  iunopn  12169  unopn  12172  eltg  12221  eltg2  12222  tgcl  12233  tgiun  12242  tgidm  12243  isopn3i  12304  isneip  12315  neipsm  12323  restbasg  12337  restopn2  12352  lmbrf  12384  cnclima  12392  lmss  12415  txbasval  12436  txlm  12448  psmetxrge0  12501  blininf  12593  blssps  12596  blss  12597  elmopn2  12618  bdmet  12671  metrest  12675  bl2ioo  12711  dvcjbr  12841  efper  12888  sinperlem  12889  abssinper  12927  bj-inex  13105  peano5set  13138  findset  13143  bj-findis  13177  nninfsellemsuc  13208  nninfself  13209  cvgcmp2nlemabs  13227  trilpolemeq1  13233