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  7451  pm54.43  7536  pw1if  7584  addclpi  7694  addasspig  7697  mulasspig  7699  distrpig  7700  mulcanpig  7702  nnppipi  7710  enqdc1  7729  addassnqg  7749  ltbtwnnqq  7782  prarloclemarch  7785  prarloclemarch2  7786  enq0sym  7799  enq0ref  7800  addclnq0  7818  nqpnq0nq  7820  nnanq0  7825  distrnq0  7826  addassnq0lemcl  7828  addassnq0  7829  distnq0r  7830  prarloclemlt  7860  genpassl  7891  genpassu  7892  genpassg  7893  nqpru  7919  addcomprg  7945  mulcomprg  7947  distrlem1prl  7949  distrlem1pru  7950  1idprl  7957  1idpru  7958  recexprlemdisj  7997  recexprlem1ssl  8000  peano2nnnn  8220  ax1rid  8244  axcaucvglemcl  8262  le2tri3i  8435  add4  8488  cnegexlem1  8502  cnegexlem3  8504  cnegex  8505  subadd  8530  addsub  8538  addsubeq4  8542  negdi  8584  renegcl  8588  resubcl  8591  subdi  8713  mulneg2  8724  mul2neg  8726  submul2  8727  ltnegcon2  8793  lenegcon2  8796  lesub0  8808  cru  8932  recextlem1  8981  recexap  8983  div12ap  9026  divnegap  9038  letrp1  9180  dfinfre  9288  peano2nn  9318  nndivre  9342  nnsub  9345  nndivtr  9348  arch  9564  bndndx  9566  nn0addge1  9613  nn0addge2  9614  zaddcl  9688  zsubcl  9689  zltnle  9694  zrevaddcl  9699  nzadd  9701  zleltp1  9704  zltlem1  9706  zdiv  9738  peano2uz2  9757  uzind  9761  eluzp1l  9956  ublbneg  10022  qaddcl  10044  qsubcl  10047  qreccl  10051  qdivcl  10052  qrevaddcl  10053  irradd  10055  irrmul  10057  rerpdivcl  10095  nn0ledivnn  10178  xrre  10232  rexsub  10265  xaddass  10281  xnpcan  10284  xsubge0  10293  xposdif  10294  elioc2  10348  icoshft  10402  iccdil  10410  fzss2  10480  fzsuc2  10496  fzrev2  10502  elfzm11  10508  elfzp1b  10514  fzrevral  10522  fzshftral  10525  fzof  10561  fzoval  10565  fzon  10584  elfzoextl  10619  fzosubel  10622  zpnn0elfzo  10635  elfzom1b  10657  qltnle  10688  flapcl  10721  flaplelt  10723  flqlt  10731  flqbi  10738  flqaddz  10745  fzofig  10882  seq3feq2  10926  ser3le  10987  expp1  10996  expm1t  11017  expeq0  11020  binom2sub  11103  bernneq  11111  expnlbnd  11115  zzlesq  11159  faccl  11187  facdiv  11190  bcpasc  11218  bccl  11219  ffz0hash  11290  fnfzo0hash  11292  hashfibclem  11296  hashf1lem2  11300  wrdlen1  11356  wrdred1  11361  ccatval21sw  11387  wrdl1exs1  11411  ccatws1cl  11414  ccatws1leng  11416  pfxmpt  11466  pfxfv  11470  pfxfvlsw  11481  ccatpfx  11487  pfx1  11489  swrdccatin1  11511  swrdccat  11521  pfxccatpfx1  11522  2shfti  11610  crim  11637  mulreap  11643  resub  11649  imsub  11657  ipcnval  11665  cjsub  11671  resqrexlemfp1  11789  resqrexlemgt0  11800  sqabsadd  11835  sqabssub  11836  abs2dif2  11888  cau3lem  11895  icodiamlt  11961  xrmaxaddlem  12042  clim  12063  clim2  12065  clim2c  12066  clim0c  12068  2clim  12083  climabs0  12089  climcn1  12090  climcn2  12091  climsqz  12117  climsqz2  12118  climub  12126  climserle  12127  fsum3cvg  12161  fisumss  12175  fsum3ser  12180  sumsplitdc  12215  fsump1i  12216  fsumlessfi  12243  telfsumo  12249  fsumparts  12253  iserabs  12258  binomlem  12266  isumsplit  12274  isum1p  12275  isumlessdc  12279  mertenslem2  12319  mertensabs  12320  prodfap0  12328  prodfrecap  12329  prodfdivap  12330  fproddccvg  12355  prodmodclem2  12360  fprodssdc  12373  fprodabs  12399  fprodeq0  12400  fprodeq0g  12421  ege2le3  12454  efsub  12464  efexp  12465  efsep  12474  sinsub  12523  cossub  12524  demoivre  12556  eirraplem  12560  moddvds  12582  0dvds  12594  iddvdsexp  12598  dvdssub  12621  dvdsle  12627  dvdsleabs  12628  dvdseq  12631  dvdsflip  12634  mulsucdiv2z  12668  divalgb  12708  divalg2  12709  ndvdsadd  12714  bitsp1  12734  gcdneg  12775  gcdabs2  12783  modgcd  12784  bezoutlemsup  12802  gcdmultiplez  12814  gcdeq  12816  dvdssq  12824  lcmcllem  12861  lcmneg  12868  lcmdvds  12873  qredeu  12891  cncongrcoprm  12900  isprm3  12912  prmrp  12940  divnumden  12992  phiprmpw  13020  crth  13022  hashgcdlem  13036  hashgcdeq  13038  modprminv  13048  modprminveq  13049  modprmn0modprm0  13055  coprimeprodsq2  13057  pcpre1  13091  pccl  13098  pcmul  13100  pcdiv  13101  pcqcl  13105  pcexp  13108  pcdvds  13114  pcndvds  13116  pcndvds2  13118  pcelnn  13120  pcgcd1  13127  pc2dvds  13129  pc11  13130  gzsubcl  13179  4sqlem3  13189  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemodife  13289  ballotfilemfrceq  13321  setsresg  13439  xpsfeq  13715  submcl  13835  grpinvnzcl  13926  mulgnnass  14009  nmzsubg  14062  nmznsg  14065  resghm2b  14114  ghmnsgpreima  14121  gzsumsnfd  14196  pwssnf1o  14260  iscrng2  14368  subrngpropd  14573  issubrg3  14604  subrgpropd  14610  islmodd  14678  lss1d  14769  lspsncl  14778  lspsnid  14793  df2idl2  14895  2idlcpbl  14910  qusrhm  14914  iunopn  15152  unopn  15155  eltg  15202  eltg2  15203  tgcl  15214  tgiun  15223  tgidm  15224  isopn3i  15285  isneip  15296  neipsm  15304  restbasg  15318  restopn2  15333  lmbrf  15365  cnclima  15373  lmss  15396  txbasval  15417  txlm  15429  psmetxrge0  15482  blininf  15574  blssps  15577  blss  15578  elmopn2  15599  bdmet  15652  metrest  15656  bl2ioo  15700  dvcjbr  15858  plyaddlem1  15897  plymullem1  15898  plyreres  15914  dvply1  15915  dvply2g  15916  efper  15958  sinperlem  15959  abssinper  15997  cxpexprp  16050  logcxp  16052  rpcxpcl  16058  rpcxproot  16069  rprelogbmulexp  16111  log2tlbndlog2  16139  bposlem2  16210  lgsval2lem  16227  lgssq2  16258  lgsprme0  16259  ausgrusgrben  16507  wlkepvtx  16714  bj-inex  17031  peano5set  17064  findset  17069  bj-findis  17103  nninfsellemsuc  17153  nninfself  17154  cvgcmp2nlemabs  17179  iooref1o  17181  trilpolemeq1  17187  nconstwlpolemgt0  17212