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 )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  sylan2b  287  sylan2br  288  syl2an  289  sylanr1  404  sylanr2  405  mpanr2  438  adantrl  478  adantrr  479  ancom2s  568  annimdc  945  ifpnst  996  3adantr1  1182  3adantr2  1183  3adantr3  1184  syl3anr1  1325  syl3anr3  1327  dfbi3dc  1441  xordidc  1443  elabgt  2946  sbciegft  3061  csbtt  3138  csbnestgf  3179  copsex2t  4336  pofun  4408  onsucmin  4604  onsucelsucr  4605  onsucsssucr  4606  ordsucunielexmid  4628  ordsuc  4660  nlimsucg  4663  elnn  4703  xpsspw  4837  elxp4  5223  elxp5  5224  funimass2  5407  imain  5411  funimaexg  5413  f1ff1  5550  dff1o2  5588  resdif  5605  funbrfv  5682  fnbrfvb2  5688  fvelimab  5702  eqfnfv2  5745  fvimacnvi  5761  ffvresb  5810  fnressn  5840  fmptapd  5845  fnex  5876  rexima  5897  ralima  5898  f1elima  5916  fnotovb  6066  mpoeq12  6083  fovcdm  6167  fnovrn  6172  ofrfval  6246  ofvalg  6247  cofunexg  6273  cofunex2g  6274  mpoexxg  6377  mpoexg  6378  f1o2ndf1  6395  spc2ed  6400  smodm2  6463  tfrlem9  6487  tfrlemibxssdm  6495  tfr1onlembxssdm  6511  tfrcllembxssdm  6524  tfri3  6535  rdgtfr  6542  rdgruledefgg  6543  oav2  6633  oasuc  6634  omv2  6635  onasuc  6636  omsuc  6642  onmsuc  6643  nnaass  6655  nndi  6656  nndir  6660  nnaword  6681  ecelqsg  6759  iinerm  6778  ecovass  6815  ecoviass  6816  ecovdi  6817  ecovidi  6818  fvdiagfn  6864  ixpssmap2g  6898  domentr  6967  xpdom1g  7019  fopwdom  7024  ssenen  7039  phplem3  7042  phplem4  7043  php5dom  7051  ssfilem  7064  ssfilemd  7066  diffitest  7078  ctssdccl  7312  pm54.43  7397  pw1if  7445  addclpi  7549  addasspig  7552  mulasspig  7554  distrpig  7555  mulcanpig  7557  nnppipi  7565  enqdc1  7584  addassnqg  7604  ltbtwnnqq  7637  prarloclemarch  7640  prarloclemarch2  7641  enq0sym  7654  enq0ref  7655  addclnq0  7673  nqpnq0nq  7675  nnanq0  7680  distrnq0  7681  addassnq0lemcl  7683  addassnq0  7684  distnq0r  7685  prarloclemlt  7715  genpassl  7746  genpassu  7747  genpassg  7748  nqpru  7774  addcomprg  7800  mulcomprg  7802  distrlem1prl  7804  distrlem1pru  7805  1idprl  7812  1idpru  7813  recexprlemdisj  7852  recexprlem1ssl  7855  peano2nnnn  8075  ax1rid  8099  axcaucvglemcl  8117  le2tri3i  8290  add4  8342  cnegexlem1  8356  cnegexlem3  8358  cnegex  8359  subadd  8384  addsub  8392  addsubeq4  8396  negdi  8438  renegcl  8442  resubcl  8445  subdi  8566  mulneg2  8577  mul2neg  8579  submul2  8580  ltnegcon2  8646  lenegcon2  8649  lesub0  8661  cru  8784  recextlem1  8833  recexap  8835  div12ap  8876  divnegap  8888  letrp1  9030  dfinfre  9138  peano2nn  9157  nndivre  9181  nnsub  9184  nndivtr  9187  arch  9401  bndndx  9403  nn0addge1  9450  nn0addge2  9451  zaddcl  9521  zsubcl  9522  zltnle  9527  zrevaddcl  9532  nzadd  9534  zleltp1  9537  zltlem1  9539  zdiv  9570  peano2uz2  9589  uzind  9593  eluzp1l  9783  ublbneg  9849  qaddcl  9871  qsubcl  9874  qreccl  9878  qdivcl  9879  qrevaddcl  9880  irradd  9882  irrmul  9883  rerpdivcl  9921  nn0ledivnn  10004  xrre  10057  rexsub  10090  xaddass  10106  xnpcan  10109  xsubge0  10118  xposdif  10119  elioc2  10173  icoshft  10227  iccdil  10235  fzss2  10301  fzsuc2  10316  fzrev2  10322  elfzm11  10328  elfzp1b  10334  fzrevral  10342  fzshftral  10345  fzof  10381  fzoval  10385  fzon  10404  elfzoextl  10439  fzosubel  10442  zpnn0elfzo  10455  elfzom1b  10477  qltnle  10506  flqlt  10546  flqbi  10553  flqaddz  10560  fzofig  10697  seq3feq2  10741  ser3le  10802  expp1  10811  expm1t  10832  expeq0  10835  binom2sub  10918  bernneq  10925  expnlbnd  10929  zzlesq  10973  faccl  11000  facdiv  11003  bcpasc  11031  bccl  11032  ffz0hash  11100  fnfzo0hash  11102  wrdlen1  11157  wrdred1  11162  ccatval21sw  11188  wrdl1exs1  11212  ccatws1cl  11215  ccatws1leng  11217  pfxmpt  11267  pfxfv  11271  pfxfvlsw  11282  ccatpfx  11288  pfx1  11290  swrdccatin1  11312  swrdccat  11322  pfxccatpfx1  11323  2shfti  11411  crim  11438  mulreap  11444  resub  11450  imsub  11458  ipcnval  11466  cjsub  11472  resqrexlemfp1  11589  resqrexlemgt0  11600  sqabsadd  11635  sqabssub  11636  abs2dif2  11687  cau3lem  11694  icodiamlt  11760  xrmaxaddlem  11840  clim  11861  clim2  11863  clim2c  11864  clim0c  11866  2clim  11881  climabs0  11887  climcn1  11888  climcn2  11889  climsqz  11915  climsqz2  11916  climub  11924  climserle  11925  fsum3cvg  11959  fisumss  11973  fsum3ser  11978  sumsplitdc  12013  fsump1i  12014  fsumlessfi  12041  telfsumo  12047  fsumparts  12051  iserabs  12056  binomlem  12064  isumsplit  12072  isum1p  12073  isumlessdc  12077  mertenslem2  12117  mertensabs  12118  prodfap0  12126  prodfrecap  12127  prodfdivap  12128  fproddccvg  12153  prodmodclem2  12158  fprodssdc  12171  fprodabs  12197  fprodeq0  12198  fprodeq0g  12219  ege2le3  12252  efsub  12262  efexp  12263  efsep  12272  sinsub  12321  cossub  12322  demoivre  12354  eirraplem  12358  moddvds  12380  0dvds  12392  iddvdsexp  12396  dvdssub  12419  dvdsle  12425  dvdsleabs  12426  dvdseq  12429  dvdsflip  12432  mulsucdiv2z  12466  divalgb  12506  divalg2  12507  ndvdsadd  12512  bitsp1  12532  gcdneg  12573  gcdabs2  12581  modgcd  12582  bezoutlemsup  12600  gcdmultiplez  12612  gcdeq  12614  dvdssq  12622  lcmcllem  12659  lcmneg  12666  lcmdvds  12671  qredeu  12689  cncongrcoprm  12698  isprm3  12710  prmrp  12737  divnumden  12788  phiprmpw  12814  crth  12816  hashgcdlem  12830  hashgcdeq  12832  modprminv  12842  modprminveq  12843  modprmn0modprm0  12849  coprimeprodsq2  12851  pcpre1  12885  pccl  12892  pcmul  12894  pcdiv  12895  pcqcl  12899  pcexp  12902  pcdvds  12908  pcndvds  12910  pcndvds2  12912  pcelnn  12914  pcgcd1  12921  pc2dvds  12923  pc11  12924  gzsubcl  12973  4sqlem3  12983  setsresg  13140  pwssnf1o  13401  xpsfeq  13448  submcl  13582  grpinvnzcl  13675  mulgnnass  13764  nmzsubg  13817  nmznsg  13820  resghm2b  13869  ghmnsgpreima  13876  gsumfzsnfd  13952  iscrng2  14049  subrngpropd  14251  issubrg3  14282  subrgpropd  14288  islmodd  14328  lss1d  14418  lspsncl  14427  lspsnid  14442  df2idl2  14544  2idlcpbl  14559  qusrhm  14563  gsumfzfsumlemm  14622  iunopn  14752  unopn  14755  eltg  14802  eltg2  14803  tgcl  14814  tgiun  14823  tgidm  14824  isopn3i  14885  isneip  14896  neipsm  14904  restbasg  14918  restopn2  14933  lmbrf  14965  cnclima  14973  lmss  14996  txbasval  15017  txlm  15029  psmetxrge0  15082  blininf  15174  blssps  15177  blss  15178  elmopn2  15199  bdmet  15252  metrest  15256  bl2ioo  15300  dvcjbr  15458  plyaddlem1  15497  plymullem1  15498  plyreres  15514  dvply1  15515  dvply2g  15516  efper  15557  sinperlem  15558  abssinper  15596  cxpexprp  15645  logcxp  15647  rpcxpcl  15653  rpcxproot  15664  rprelogbmulexp  15706  lgsval2lem  15765  lgssq2  15796  lgsprme0  15797  ausgrusgrben  16045  wlkepvtx  16252  bj-inex  16560  peano5set  16593  findset  16598  bj-findis  16632  nninfsellemsuc  16672  nninfself  16673  cvgcmp2nlemabs  16698  iooref1o  16700  trilpolemeq1  16706  nconstwlpolemgt0  16731