Theorem sylan2 280

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  sylan2b  281  sylan2br  282  syl2an  283  sylanr1  396  sylanr2  397  mpanr2  428  adantrl  461  adantrr  462  ancom2s  530  3adantr1  1097  3adantr2  1098  3adantr3  1099  syl3anr1  1221  syl3anr3  1223  dfbi3dc  1328  xordidc  1330  elabgt  2735  sbciegft  2844  csbtt  2918  csbnestgf  2954  copsex2t  4000  pofun  4067  onsucmin  4251  onsucelsucr  4252  onsucsssucr  4253  ordsucunielexmid  4274  ordsuc  4306  nlimsucg  4309  elnn  4346  xpsspw  4468  elxp4  4828  elxp5  4829  funimass2  4997  imain  5001  funimaexg  5003  dff1o2  5151  resdif  5168  funbrfv  5233  fvelimab  5250  eqfnfv2  5287  fvimacnvi  5302  ffvresb  5349  fnressn  5370  fmptapd  5375  fnex  5404  rexima  5415  ralima  5416  f1elima  5433  fnotovb  5568  mpt2eq12  5585  fovrn  5663  fnovrn  5668  ofrfval  5740  fnofval  5741  cofunexg  5758  cofunex2g  5759  mpt2exxg  5853  mpt2exg  5854  f1o2ndf1  5869  spc2ed  5874  smodm2  5933  tfrlem9  5958  tfrlemibxssdm  5964  tfri3  5976  rdgtfr  5984  rdgruledefgg  5985  frecsuclem1  6010  oav2  6066  oasuc  6067  omv2  6068  onasuc  6069  omsuc  6074  onmsuc  6075  nnaass  6087  nndi  6088  nndir  6092  nnaword  6107  ecelqsg  6182  iinerm  6201  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  domentr  6294  xpdom1g  6330  fopwdom  6333  phplem3  6340  phplem4  6341  php5dom  6349  ssfilem  6360  diffitest  6371  pm54.43  6459  addclpi  6517  addasspig  6520  mulasspig  6522  distrpig  6523  mulcanpig  6525  nnppipi  6533  enqdc1  6552  addassnqg  6572  ltbtwnnqq  6605  prarloclemarch  6608  prarloclemarch2  6609  enq0sym  6622  enq0ref  6623  addclnq0  6641  nqpnq0nq  6643  nnanq0  6648  distrnq0  6649  addassnq0lemcl  6651  addassnq0  6652  distnq0r  6653  prarloclemlt  6683  genpassl  6714  genpassu  6715  genpassg  6716  nqpru  6742  addcomprg  6768  mulcomprg  6770  distrlem1prl  6772  distrlem1pru  6773  1idprl  6780  1idpru  6781  recexprlemdisj  6820  recexprlem1ssl  6823  peano2nnnn  7021  ax1rid  7043  axcaucvglemcl  7061  le2tri3i  7219  add4  7269  cnegexlem1  7283  cnegexlem3  7285  cnegex  7286  subadd  7311  addsub  7319  addsubeq4  7323  negdi  7365  renegcl  7369  resubcl  7372  subdi  7489  mulneg2  7500  mul2neg  7502  submul2  7503  ltnegcon2  7568  lenegcon2  7571  lesub0  7583  cru  7702  recextlem1  7741  recexap  7743  div12ap  7782  divnegap  7794  letrp1  7926  dfinfre  8034  peano2nn  8051  nndivre  8074  nnsub  8077  nndivtr  8080  arch  8285  bndndx  8287  nn0addge1  8334  nn0addge2  8335  zaddcl  8391  zsubcl  8392  zltnle  8397  zrevaddcl  8401  nzadd  8403  zleltp1  8406  zltlem1  8408  zdiv  8435  peano2uz2  8454  uzind  8458  eluzp1l  8643  ublbneg  8698  qaddcl  8720  qsubcl  8723  qreccl  8727  qdivcl  8728  qrevaddcl  8729  irradd  8731  irrmul  8732  rerpdivcl  8764  nn0ledivnn  8838  xrre  8887  elioc2  8959  icoshft  9012  iccdil  9020  fzss2  9082  fzsuc2  9096  fzrev2  9102  elfzm11  9108  elfzp1b  9114  fzrevral  9122  fzshftral  9125  fzof  9154  fzoval  9158  fzon  9175  fzosubel  9203  zpnn0elfzo  9216  elfzom1b  9238  qltnle  9255  flqlt  9285  flqbi  9292  flqaddz  9299  fzofig  9424  iseqfeq2  9449  iseqfeq  9451  iseqsplit  9458  expp1  9483  expm1t  9504  expeq0  9507  binom2sub  9587  bernneq  9593  expnlbnd  9597  faccl  9662  facdiv  9665  bcpasc  9693  bccl  9694  2shfti  9719  crim  9745  mulreap  9751  resub  9757  imsub  9765  ipcnval  9773  cjsub  9779  resqrexlemfp1  9895  resqrexlemgt0  9906  sqabsadd  9941  sqabssub  9942  abs2dif2  9993  cau3lem  10000  icodiamlt  10066  clim  10120  clim2  10122  clim2c  10123  clim0c  10125  2clim  10140  climabs0  10146  climcn1  10147  climcn2  10148  climsqz  10173  climsqz2  10174  climub  10182  climserile  10183  moddvds  10204  0dvds  10215  iddvdsexp  10219  dvdssub  10240  dvdsle  10244  dvdsleabs  10245  dvdseq  10248  dvdsflip  10251  mulsucdiv2z  10285  divalgb  10325  divalg2  10326  ndvdsadd  10331  gcdneg  10373  gcdabs2  10381  modgcd  10382  bezoutlemsup  10398  gcdmultiplez  10410  gcdeq  10412  dvdssq  10420  lcmcllem  10449  lcmneg  10456  lcmdvds  10461  qredeu  10479  cncongrcoprm  10488  isprm3  10500  prmrp  10524  bj-inex  10698  peano5set  10735  findset  10740  bj-findis  10774