ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan2 Unicode version

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
StepHypRef Expression
1 sylan2.1 . . 3  |-  ( ph  ->  ch )
21adantl 271 . 2  |-  ( ( ps  /\  ph )  ->  ch )
3 sylan2.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3syldan 276 1  |-  ( ( ps  /\  ph )  ->  th )
Colors of variables: wff set class
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  429  adantrl  462  adantrr  463  ancom2s  531  3adantr1  1098  3adantr2  1099  3adantr3  1100  syl3anr1  1222  syl3anr3  1224  dfbi3dc  1329  xordidc  1331  elabgt  2736  sbciegft  2845  csbtt  2919  csbnestgf  2955  copsex2t  4008  pofun  4075  onsucmin  4259  onsucelsucr  4260  onsucsssucr  4261  ordsucunielexmid  4282  ordsuc  4314  nlimsucg  4317  elnn  4354  xpsspw  4478  elxp4  4838  elxp5  4839  funimass2  5008  imain  5012  funimaexg  5014  dff1o2  5162  resdif  5179  funbrfv  5244  fvelimab  5261  eqfnfv2  5298  fvimacnvi  5313  ffvresb  5360  fnressn  5381  fmptapd  5386  fnex  5415  rexima  5426  ralima  5427  f1elima  5444  fnotovb  5579  mpt2eq12  5596  fovrn  5674  fnovrn  5679  ofrfval  5751  fnofval  5752  cofunexg  5769  cofunex2g  5770  mpt2exxg  5864  mpt2exg  5865  f1o2ndf1  5880  spc2ed  5885  smodm2  5944  tfrlem9  5968  tfrlemibxssdm  5976  tfr1onlembxssdm  5992  tfrcllembxssdm  6005  tfri3  6016  rdgtfr  6023  rdgruledefgg  6024  oav2  6107  oasuc  6108  omv2  6109  onasuc  6110  omsuc  6116  onmsuc  6117  nnaass  6129  nndi  6130  nndir  6134  nnaword  6150  ecelqsg  6225  iinerm  6244  ecovass  6281  ecoviass  6282  ecovdi  6283  ecovidi  6284  domentr  6338  xpdom1g  6377  fopwdom  6380  phplem3  6389  phplem4  6390  php5dom  6398  ssfilem  6410  diffitest  6421  pm54.43  6518  addclpi  6579  addasspig  6582  mulasspig  6584  distrpig  6585  mulcanpig  6587  nnppipi  6595  enqdc1  6614  addassnqg  6634  ltbtwnnqq  6667  prarloclemarch  6670  prarloclemarch2  6671  enq0sym  6684  enq0ref  6685  addclnq0  6703  nqpnq0nq  6705  nnanq0  6710  distrnq0  6711  addassnq0lemcl  6713  addassnq0  6714  distnq0r  6715  prarloclemlt  6745  genpassl  6776  genpassu  6777  genpassg  6778  nqpru  6804  addcomprg  6830  mulcomprg  6832  distrlem1prl  6834  distrlem1pru  6835  1idprl  6842  1idpru  6843  recexprlemdisj  6882  recexprlem1ssl  6885  peano2nnnn  7083  ax1rid  7105  axcaucvglemcl  7123  le2tri3i  7286  add4  7336  cnegexlem1  7350  cnegexlem3  7352  cnegex  7353  subadd  7378  addsub  7386  addsubeq4  7390  negdi  7432  renegcl  7436  resubcl  7439  subdi  7556  mulneg2  7567  mul2neg  7569  submul2  7570  ltnegcon2  7635  lenegcon2  7638  lesub0  7650  cru  7769  recextlem1  7808  recexap  7810  div12ap  7849  divnegap  7861  letrp1  7993  dfinfre  8101  peano2nn  8118  nndivre  8141  nnsub  8144  nndivtr  8147  arch  8352  bndndx  8354  nn0addge1  8401  nn0addge2  8402  zaddcl  8472  zsubcl  8473  zltnle  8478  zrevaddcl  8482  nzadd  8484  zleltp1  8487  zltlem1  8489  zdiv  8516  peano2uz2  8535  uzind  8539  eluzp1l  8724  ublbneg  8779  qaddcl  8801  qsubcl  8804  qreccl  8808  qdivcl  8809  qrevaddcl  8810  irradd  8812  irrmul  8813  rerpdivcl  8845  nn0ledivnn  8919  xrre  8963  elioc2  9035  icoshft  9088  iccdil  9096  fzss2  9158  fzsuc2  9172  fzrev2  9178  elfzm11  9184  elfzp1b  9190  fzrevral  9198  fzshftral  9201  fzof  9231  fzoval  9235  fzon  9252  fzosubel  9280  zpnn0elfzo  9293  elfzom1b  9315  qltnle  9332  flqlt  9365  flqbi  9372  flqaddz  9379  fzofig  9514  iseqfeq2  9545  iseqfeq  9547  iseqsplit  9554  expp1  9580  expm1t  9601  expeq0  9604  binom2sub  9684  bernneq  9690  expnlbnd  9694  faccl  9759  facdiv  9762  bcpasc  9790  bccl  9791  2shfti  9857  crim  9883  mulreap  9889  resub  9895  imsub  9903  ipcnval  9911  cjsub  9917  resqrexlemfp1  10033  resqrexlemgt0  10044  sqabsadd  10079  sqabssub  10080  abs2dif2  10131  cau3lem  10138  icodiamlt  10204  clim  10258  clim2  10260  clim2c  10261  clim0c  10263  2clim  10278  climabs0  10284  climcn1  10285  climcn2  10286  climsqz  10311  climsqz2  10312  climub  10320  climserile  10321  fisumcvg  10338  moddvds  10349  0dvds  10360  iddvdsexp  10364  dvdssub  10385  dvdsle  10389  dvdsleabs  10390  dvdseq  10393  dvdsflip  10396  mulsucdiv2z  10429  divalgb  10469  divalg2  10470  ndvdsadd  10475  gcdneg  10517  gcdabs2  10525  modgcd  10526  bezoutlemsup  10542  gcdmultiplez  10554  gcdeq  10556  dvdssq  10564  lcmcllem  10593  lcmneg  10600  lcmdvds  10605  qredeu  10623  cncongrcoprm  10632  isprm3  10644  prmrp  10668  bj-inex  10856  peano5set  10893  findset  10898  bj-findis  10932
  Copyright terms: Public domain W3C validator