Theorem sylan2 282

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sylan2b  283  sylan2br  284  syl2an  285  sylanr1  399  sylanr2  400  mpanr2  432  adantrl  467  adantrr  468  ancom2s  538  3adantr1  1123  3adantr2  1124  3adantr3  1125  syl3anr1  1251  syl3anr3  1253  dfbi3dc  1358  xordidc  1360  elabgt  2795  sbciegft  2907  csbtt  2981  csbnestgf  3018  copsex2t  4127  pofun  4194  onsucmin  4383  onsucelsucr  4384  onsucsssucr  4385  ordsucunielexmid  4406  ordsuc  4438  nlimsucg  4441  elnn  4479  xpsspw  4611  elxp4  4984  elxp5  4985  funimass2  5159  imain  5163  funimaexg  5165  f1ff1  5294  dff1o2  5328  resdif  5345  funbrfv  5414  fvelimab  5431  eqfnfv2  5473  fvimacnvi  5488  ffvresb  5537  fnressn  5560  fmptapd  5565  fnex  5596  rexima  5610  ralima  5611  f1elima  5628  fnotovb  5768  mpoeq12  5785  fovrn  5867  fnovrn  5872  ofrfval  5944  ofvalg  5945  cofunexg  5963  cofunex2g  5964  mpoexxg  6062  mpoexg  6063  f1o2ndf1  6079  spc2ed  6084  smodm2  6146  tfrlem9  6170  tfrlemibxssdm  6178  tfr1onlembxssdm  6194  tfrcllembxssdm  6207  tfri3  6218  rdgtfr  6225  rdgruledefgg  6226  oav2  6313  oasuc  6314  omv2  6315  onasuc  6316  omsuc  6322  onmsuc  6323  nnaass  6335  nndi  6336  nndir  6340  nnaword  6361  ecelqsg  6436  iinerm  6455  ecovass  6492  ecoviass  6493  ecovdi  6494  ecovidi  6495  fvdiagfn  6541  ixpssmap2g  6575  domentr  6639  xpdom1g  6680  fopwdom  6683  ssenen  6698  phplem3  6701  phplem4  6702  php5dom  6710  ssfilem  6722  diffitest  6734  ctssdccl  6948  pm54.43  6996  addclpi  7083  addasspig  7086  mulasspig  7088  distrpig  7089  mulcanpig  7091  nnppipi  7099  enqdc1  7118  addassnqg  7138  ltbtwnnqq  7171  prarloclemarch  7174  prarloclemarch2  7175  enq0sym  7188  enq0ref  7189  addclnq0  7207  nqpnq0nq  7209  nnanq0  7214  distrnq0  7215  addassnq0lemcl  7217  addassnq0  7218  distnq0r  7219  prarloclemlt  7249  genpassl  7280  genpassu  7281  genpassg  7282  nqpru  7308  addcomprg  7334  mulcomprg  7336  distrlem1prl  7338  distrlem1pru  7339  1idprl  7346  1idpru  7347  recexprlemdisj  7386  recexprlem1ssl  7389  peano2nnnn  7588  ax1rid  7612  axcaucvglemcl  7630  le2tri3i  7795  add4  7846  cnegexlem1  7860  cnegexlem3  7862  cnegex  7863  subadd  7888  addsub  7896  addsubeq4  7900  negdi  7942  renegcl  7946  resubcl  7949  subdi  8066  mulneg2  8077  mul2neg  8079  submul2  8080  ltnegcon2  8145  lenegcon2  8148  lesub0  8160  cru  8282  recextlem1  8325  recexap  8327  div12ap  8367  divnegap  8379  letrp1  8516  dfinfre  8624  peano2nn  8642  nndivre  8666  nnsub  8669  nndivtr  8672  arch  8878  bndndx  8880  nn0addge1  8927  nn0addge2  8928  zaddcl  8998  zsubcl  8999  zltnle  9004  zrevaddcl  9008  nzadd  9010  zleltp1  9013  zltlem1  9015  zdiv  9043  peano2uz2  9062  uzind  9066  eluzp1l  9252  ublbneg  9307  qaddcl  9329  qsubcl  9332  qreccl  9336  qdivcl  9337  qrevaddcl  9338  irradd  9340  irrmul  9341  rerpdivcl  9373  nn0ledivnn  9447  xrre  9496  rexsub  9529  xaddass  9545  xnpcan  9548  xsubge0  9557  xposdif  9558  elioc2  9612  icoshft  9666  iccdil  9674  fzss2  9737  fzsuc2  9752  fzrev2  9758  elfzm11  9764  elfzp1b  9770  fzrevral  9778  fzshftral  9781  fzof  9814  fzoval  9818  fzon  9836  fzosubel  9864  zpnn0elfzo  9877  elfzom1b  9899  qltnle  9916  flqlt  9949  flqbi  9956  flqaddz  9963  fzofig  10098  seq3feq2  10136  ser3le  10184  expp1  10193  expm1t  10214  expeq0  10217  binom2sub  10298  bernneq  10305  expnlbnd  10309  faccl  10374  facdiv  10377  bcpasc  10405  bccl  10406  ffz0hash  10469  fnfzo0hash  10471  2shfti  10496  crim  10523  mulreap  10529  resub  10535  imsub  10543  ipcnval  10551  cjsub  10557  resqrexlemfp1  10673  resqrexlemgt0  10684  sqabsadd  10719  sqabssub  10720  abs2dif2  10771  cau3lem  10778  icodiamlt  10844  xrmaxaddlem  10921  clim  10942  clim2  10944  clim2c  10945  clim0c  10947  2clim  10962  climabs0  10968  climcn1  10969  climcn2  10970  climsqz  10996  climsqz2  10997  climub  11005  climserle  11006  fsum3cvg  11038  fisumss  11053  fsum3ser  11058  sumsplitdc  11093  fsump1i  11094  fsumlessfi  11121  telfsumo  11127  fsumparts  11131  iserabs  11136  binomlem  11144  isumsplit  11152  isum1p  11153  isumlessdc  11157  mertenslem2  11197  mertensabs  11198  ege2le3  11228  efsub  11238  efexp  11239  efsep  11248  sinsub  11298  cossub  11299  demoivre  11329  eirraplem  11331  moddvds  11350  0dvds  11361  iddvdsexp  11365  dvdssub  11386  dvdsle  11390  dvdsleabs  11391  dvdseq  11394  dvdsflip  11397  mulsucdiv2z  11430  divalgb  11470  divalg2  11471  ndvdsadd  11476  gcdneg  11518  gcdabs2  11526  modgcd  11527  bezoutlemsup  11543  gcdmultiplez  11555  gcdeq  11557  dvdssq  11565  lcmcllem  11594  lcmneg  11601  lcmdvds  11606  qredeu  11624  cncongrcoprm  11633  isprm3  11645  prmrp  11669  divnumden  11719  phiprmpw  11743  crth  11745  hashgcdlem  11748  hashgcdeq  11749  setsresg  11840  iunopn  12012  unopn  12015  eltg  12064  eltg2  12065  tgcl  12076  tgiun  12085  tgidm  12086  isopn3i  12147  isneip  12158  neipsm  12166  restbasg  12180  restopn2  12195  lmbrf  12226  cnclima  12234  lmss  12257  txbasval  12278  txlm  12290  psmetxrge0  12321  blininf  12413  blssps  12416  blss  12417  elmopn2  12438  bdmet  12491  metrest  12495  bl2ioo  12528  bj-inex  12797  peano5set  12830  findset  12835  bj-findis  12869  nninfsellemsuc  12900  nninfself  12901  cvgcmp2nlemabs  12919  trilpolemeq1  12925