Theorem sylan2 286

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  408  sylanr2  409  mpanr2  442  adantrl  482  adantrr  483  ancom2s  572  annimdc  950  ifpnst  1001  3adantr1  1187  3adantr2  1188  3adantr3  1189  syl3anr1  1330  syl3anr3  1332  dfbi3dc  1446  xordidc  1448  elabgt  2967  sbciegft  3082  csbtt  3159  csbnestgf  3200  copsex2t  4385  pofun  4457  onsucmin  4654  onsucelsucr  4655  onsucsssucr  4656  ordsucunielexmid  4678  ordsuc  4710  nlimsucg  4713  elnn  4753  xpsspw  4887  elxp4  5275  elxp5  5276  funimass2  5459  imain  5463  funimaexg  5465  f1ff1  5606  dff1o2  5644  resdif  5661  funbrfv  5739  fnbrfvb2  5745  fvelimab  5759  eqfnfv2  5807  fvimacnvi  5823  ffvresb  5871  fnressn  5901  fmptapd  5906  fnex  5937  rexima  5960  ralima  5961  f1elima  5979  fnotovb  6131  mpoeq12  6148  fovcdm  6232  fnovrn  6237  ofrfval  6311  ofvalg  6312  cofunexg  6338  cofunex2g  6339  mpoexxg  6446  mpoexg  6447  f1o2ndf1  6464  spc2ed  6469  funsssuppss  6498  smodm2  6566  tfrlem9  6590  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  tfri3  6638  rdgtfr  6645  rdgruledefgg  6646  oav2  6736  oasuc  6737  omv2  6738  onasuc  6739  omsuc  6745  onmsuc  6746  nnaass  6758  nndi  6759  nndir  6763  nnaword  6784  ecelqsg  6862  iinerm  6881  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  fvdiagfn  6975  ixpssmap2g  7009  domentr  7078  xpdom1g  7131  fopwdom  7136  ssenen  7152  phplem3  7155  phplem4  7156  php5dom  7164  ssfilem  7177  ssfilemd  7179  diffitest  7191  ctssdccl  7452  pm54.43  7537  pw1if  7585  addclpi  7695  addasspig  7698  mulasspig  7700  distrpig  7701  mulcanpig  7703  nnppipi  7711  enqdc1  7730  addassnqg  7750  ltbtwnnqq  7783  prarloclemarch  7786  prarloclemarch2  7787  enq0sym  7800  enq0ref  7801  addclnq0  7819  nqpnq0nq  7821  nnanq0  7826  distrnq0  7827  addassnq0lemcl  7829  addassnq0  7830  distnq0r  7831  prarloclemlt  7861  genpassl  7892  genpassu  7893  genpassg  7894  nqpru  7920  addcomprg  7946  mulcomprg  7948  distrlem1prl  7950  distrlem1pru  7951  1idprl  7958  1idpru  7959  recexprlemdisj  7998  recexprlem1ssl  8001  peano2nnnn  8221  ax1rid  8245  axcaucvglemcl  8263  le2tri3i  8436  add4  8489  cnegexlem1  8503  cnegexlem3  8505  cnegex  8506  subadd  8531  addsub  8539  addsubeq4  8543  negdi  8585  renegcl  8589  resubcl  8592  subdi  8714  mulneg2  8725  mul2neg  8727  submul2  8728  ltnegcon2  8794  lenegcon2  8797  lesub0  8809  cru  8933  recextlem1  8982  recexap  8984  div12ap  9027  divnegap  9039  letrp1  9181  dfinfre  9289  peano2nn  9319  nndivre  9343  nnsub  9346  nndivtr  9349  arch  9565  bndndx  9567  nn0addge1  9614  nn0addge2  9615  zaddcl  9689  zsubcl  9690  zltnle  9695  zrevaddcl  9700  nzadd  9702  zleltp1  9705  zltlem1  9707  zdiv  9739  peano2uz2  9758  uzind  9762  eluzp1l  9957  ublbneg  10023  qaddcl  10045  qsubcl  10048  qreccl  10052  qdivcl  10053  qrevaddcl  10054  irradd  10056  irrmul  10058  rerpdivcl  10096  nn0ledivnn  10179  xrre  10233  rexsub  10266  xaddass  10282  xnpcan  10285  xsubge0  10294  xposdif  10295  elioc2  10349  icoshft  10403  iccdil  10411  fzss2  10481  fzsuc2  10497  fzrev2  10503  elfzm11  10509  elfzp1b  10515  fzrevral  10523  fzshftral  10526  fzof  10562  fzoval  10566  fzon  10585  elfzoextl  10620  fzosubel  10623  zpnn0elfzo  10636  elfzom1b  10658  qltnle  10689  flapcl  10722  flaplelt  10724  flqlt  10732  flqbi  10740  flqaddz  10747  fzofig  10884  seq3feq2  10928  ser3le  10989  expp1  10998  expm1t  11019  expeq0  11022  binom2sub  11105  bernneq  11113  expnlbnd  11117  zzlesq  11161  faccl  11189  facdiv  11192  bcpasc  11220  bccl  11221  ffz0hash  11292  fnfzo0hash  11294  hashfibclem  11298  hashf1lem2  11302  wrdlen1  11358  wrdred1  11363  ccatval21sw  11389  wrdl1exs1  11413  ccatws1cl  11416  ccatws1leng  11418  pfxmpt  11468  pfxfv  11472  pfxfvlsw  11483  ccatpfx  11489  pfx1  11491  swrdccatin1  11513  swrdccat  11523  pfxccatpfx1  11524  2shfti  11612  crim  11639  mulreap  11645  resub  11651  imsub  11659  ipcnval  11667  cjsub  11673  resqrexlemfp1  11791  resqrexlemgt0  11802  sqabsadd  11837  sqabssub  11838  abs2dif2  11890  cau3lem  11897  icodiamlt  11963  xrmaxaddlem  12045  clim  12066  clim2  12068  clim2c  12069  clim0c  12071  2clim  12086  climabs0  12092  climcn1  12093  climcn2  12094  climsqz  12120  climsqz2  12121  climub  12129  climserle  12130  fsum3cvg  12164  fisumss  12178  fsum3ser  12183  sumsplitdc  12218  fsump1i  12219  fsumlessfi  12246  telfsumo  12252  fsumparts  12256  iserabs  12261  binomlem  12269  isumsplit  12277  isum1p  12278  isumlessdc  12282  mertenslem2  12322  mertensabs  12323  prodfap0  12331  prodfrecap  12332  prodfdivap  12333  fproddccvg  12358  prodmodclem2  12363  fprodssdc  12376  fprodabs  12402  fprodeq0  12403  fprodeq0g  12424  ege2le3  12457  efsub  12467  efexp  12468  efsep  12477  sinsub  12526  cossub  12527  demoivre  12559  eirraplem  12563  moddvds  12585  0dvds  12597  iddvdsexp  12601  dvdssub  12624  dvdsle  12630  dvdsleabs  12631  dvdseq  12634  dvdsflip  12637  mulsucdiv2z  12671  divalgb  12711  divalg2  12712  ndvdsadd  12717  bitsp1  12737  gcdneg  12778  gcdabs2  12786  modgcd  12787  bezoutlemsup  12805  gcdmultiplez  12817  gcdeq  12819  dvdssq  12827  lcmcllem  12864  lcmneg  12871  lcmdvds  12876  qredeu  12894  cncongrcoprm  12903  isprm3  12915  prmrp  12943  divnumden  12995  phiprmpw  13023  crth  13025  hashgcdlem  13039  hashgcdeq  13041  modprminv  13051  modprminveq  13052  modprmn0modprm0  13058  coprimeprodsq2  13060  pcpre1  13094  pccl  13101  pcmul  13103  pcdiv  13104  pcqcl  13108  pcexp  13111  pcdvds  13117  pcndvds  13119  pcndvds2  13121  pcelnn  13123  pcgcd1  13130  pc2dvds  13132  pc11  13133  gzsubcl  13182  4sqlem3  13192  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemodife  13292  ballotfilemfrceq  13324  setsresg  13442  xpsfeq  13719  submcl  13839  grpinvnzcl  13930  mulgnnass  14013  nmzsubg  14066  nmznsg  14069  resghm2b  14118  ghmnsgpreima  14125  gzsumsnfd  14231  pwssnf1o  14295  iscrng2  14403  subrngpropd  14608  issubrg3  14639  subrgpropd  14645  islmodd  14713  lss1d  14804  lspsncl  14813  lspsnid  14828  df2idl2  14930  2idlcpbl  14945  qusrhm  14949  iunopn  15194  unopn  15197  eltg  15244  eltg2  15245  tgcl  15256  tgiun  15265  tgidm  15266  isopn3i  15327  isneip  15338  neipsm  15346  restbasg  15360  restopn2  15375  lmbrf  15407  cnclima  15415  lmss  15438  txbasval  15459  txlm  15471  psmetxrge0  15524  blininf  15616  blssps  15619  blss  15620  elmopn2  15641  bdmet  15694  metrest  15698  bl2ioo  15742  dvcjbr  15900  plyaddlem1  15939  plymullem1  15940  plyreres  15956  dvply1  15957  dvply2g  15958  efper  16000  sinperlem  16001  abssinper  16039  cxpexprp  16092  logcxp  16094  rpcxpcl  16100  rpcxproot  16111  rprelogbmulexp  16153  log2tlbndlog2  16181  prmorcht  16243  bposlem2  16273  bpos  16281  lgsval2lem  16295  lgssq2  16326  lgsprme0  16327  ausgrusgrben  16575  wlkepvtx  16782  bj-inex  17099  peano5set  17132  findset  17137  bj-findis  17171  nninfsellemsuc  17221  nninfself  17222  cvgcmp2nlemabs  17247  iooref1o  17249  trilpolemeq1  17256  nconstwlpolemgt0  17281