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

Theorem sylan 277
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
Hypotheses
Ref Expression
sylan.1  |-  ( ph  ->  ps )
sylan.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylan  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem sylan
StepHypRef Expression
1 sylan.1 . 2  |-  ( ph  ->  ps )
2 sylan.2 . . 3  |-  ( ( ps  /\  ch )  ->  th )
32expcom 114 . 2  |-  ( ch 
->  ( ps  ->  th )
)
41, 3mpan9 275 1  |-  ( (
ph  /\  ch )  ->  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:  sylanb  278  sylanbr  279  syl2an  283  sylanl1  394  sylanl2  395  mpanl1  425  mpanl2  426  adantll  460  adantlr  461  ancom1s  534  3adantl1  1095  3adantl2  1096  3adantl3  1097  syl3anl1  1218  syl3anl3  1220  syl3anl  1221  stoic3  1361  eupick  2022  csbiebt  2953  csbnestgf  2965  reuss2  3262  mpteq12  3887  otexg  4021  opelopabt  4053  sonr  4108  sotr  4109  issod  4110  so2nr  4112  so3nr  4113  ordelss  4170  onelon  4175  elrnmpt1s  4643  iota2  4960  funeu  4993  imadif  5047  fnbr  5069  feu  5141  f1ss  5170  f1ssres  5173  f1resf1  5174  dffo2  5185  foco  5191  foun  5220  fun11iun  5222  ffoss  5233  funbrfv  5288  fvco3  5320  fvopab6  5341  funfvbrb  5357  elpreima  5363  ffvelrn  5377  ffvelrnda  5379  dffo4  5392  fmptco  5406  fsn2  5413  fvconst2g  5451  fex  5464  funfvima  5466  foelrnOLD  5472  f1elima  5492  f1ocnvfv1  5496  f1ocnvfv2  5497  cocan2  5507  foeqcnvco  5509  isocnv  5530  isores2  5532  isoini  5536  isoselem  5538  f1oiso  5544  f1ofveu  5579  eloprabga  5670  grprinvlem  5774  suppssof1  5807  ofco  5808  offveqb  5809  fnexALT  5819  f1dmex  5822  ot1stg  5858  ot2ndg  5859  ot3rdgg  5860  eqopi  5877  2ndrn  5888  fo2ndf  5927  smores3  5990  smores2  5991  smoel  5997  smoiso  5999  tfrlem1  6005  tfrlemisucaccv  6022  tfrlemibxssdm  6024  tfrlemiubacc  6027  tfr1onlemsucaccv  6038  tfr1onlembfn  6041  tfr1onlemubacc  6043  tfr1onlemaccex  6045  tfr1onlemres  6046  tfrcllemsucaccv  6051  tfrcllembfn  6054  tfrcllemubacc  6056  tfrcllemaccex  6058  tfrcllemres  6059  tfrcl  6061  frecrdg  6105  omv2  6158  nnasuc  6169  nnmsuc  6170  nnacom  6177  nnaass  6178  nnmass  6180  nntri1  6189  nndifsnid  6196  nnmordi  6205  swoer  6250  erth  6266  riinerm  6295  qliftlem  6300  ecovass  6331  ecoviass  6332  elmapssres  6360  f1domg  6405  endomtr  6437  xpsnen2g  6475  enen1  6486  enen2  6487  domen1  6488  domen2  6489  mapen  6492  mapxpen  6494  ssenen  6497  phplem1  6498  fidifsnid  6517  findcard  6534  findcard2  6535  findcard2s  6536  isotilem  6608  supisolem  6610  inflbti  6626  ordiso2  6635  djuex  6643  updjudhcoinlf  6678  updjudhcoinrg  6679  updjud  6680  finomni  6701  pm54.43  6721  addclpi  6789  addasspig  6792  mulasspig  6794  addnidpig  6798  nnppipi  6805  ltanqi  6864  ltmnqi  6865  ltexnqq  6870  archnqq  6879  prarloclemarch2  6881  enq0sym  6894  enq0tr  6896  nqnq0pi  6900  nqnq0  6903  mulcanenq0ec  6907  addclnq0  6913  nqpnq0nq  6915  distrnq0  6921  addassnq0lemcl  6923  addassnq0  6924  prubl  6948  prarloclemlt  6955  genpdf  6970  genipv  6971  genpelvl  6974  genpelvu  6975  genpml  6979  genpmu  6980  genprndl  6983  genprndu  6984  genpassl  6986  genpassu  6987  genpassg  6988  addnqprl  6991  addnqpru  6992  addlocpr  6998  nqprm  7004  nqprl  7013  nqpru  7014  mulnqprl  7030  mulnqpru  7031  mullocprlem  7032  mullocpr  7033  addcomprg  7040  mulcomprg  7042  distrlem1prl  7044  distrlem1pru  7045  distrlem4prl  7046  distrlem4pru  7047  ltprordil  7051  1idprl  7052  1idpru  7053  ltpopr  7057  ltsopr  7058  ltaddpr  7059  ltexprlemm  7062  ltexprlemopl  7063  ltexprlemlol  7064  ltexprlemopu  7065  ltexprlemupu  7066  ltexprlemdisj  7068  ltexprlemloc  7069  ltexprlemfl  7071  ltexprlemrl  7072  ltexprlemfu  7073  ltexprlemru  7074  addcanprleml  7076  addcanprlemu  7077  prplnqu  7082  recexprlemloc  7093  recexprlem1ssl  7095  recexprlem1ssu  7096  recexprlemss1l  7097  recexprlemss1u  7098  aptiprleml  7101  aptiprlemu  7102  cauappcvgprlemloc  7114  cauappcvgprlemladdru  7118  cauappcvgprlemladdrl  7119  caucvgprlemloc  7137  caucvgprlemladdrl  7140  caucvgprprlemml  7156  caucvgprprlemloc  7165  00sr  7218  adddir  7382  eqle  7479  le2tri3i  7496  mul4  7517  muladd11  7518  cnegexlem3  7562  addsub12  7598  2addsub  7599  addsubeq4  7600  subadd4  7629  negcon1  7637  negdi2  7643  negsubdi2  7644  neg2sub  7645  renegcl  7646  muladd  7765  subdir  7767  gt0ne0  7808  ltnegcon1  7844  lenegcon1  7847  recexre  7955  ltmul1  7969  recexap  8020  div12ap  8059  p1le  8204  ltmul2  8211  gt0div  8225  ge0div  8226  nnnninf  8645  zlem1lt  8702  nnaddm1cl  8707  zdceq  8718  gtndiv  8737  prime  8741  msqznn  8742  btwnz  8761  uzss  8934  eluzadd  8942  nn0pzuz  8970  supinfneg  8978  infsupneg  8979  divfnzn  9001  qnegcl  9016  qreccl  9022  elico2  9250  iccss  9254  iccsupr  9279  elfz5  9327  fznn  9396  difelfznle  9437  fzoaddel  9492  qdceq  9547  qbtwnxr  9558  flqbi2  9587  adddivflid  9588  fldivnn0  9591  divfl0  9592  flqmulnn0  9595  fldivnn0le  9599  fldiv4p1lem1div2  9601  ceiqle  9609  flqdiv  9617  modqmulnn  9638  frecuzrdgtcl  9708  frecuzrdgsuc  9710  frecuzrdgdomlem  9713  frecuzrdgfunlem  9715  frecuzrdgsuctlem  9719  iseqsplit  9773  iseqcaopr2  9776  iseqid  9782  iseqz  9785  expap0  9822  mulexp  9831  mulexpzap  9832  expmul  9837  leexp1a  9847  expubnd  9849  zesq  9907  bernneq  9909  bernneq3  9911  facdiv  9981  facndiv  9982  faclbnd3  9986  faclbnd6  9987  bccmpl  9997  bcpasc  10009  bccl  10010  shftlem  10078  ovshftex  10081  shftval4  10090  shftf  10092  shftcan2  10097  crim  10119  mulreap  10125  remul2  10134  immul2  10141  cjexp  10154  caucvgre  10241  r19.2uz  10253  sqrtsq2  10303  absnid  10333  absexp  10339  nn0abscl  10345  abslt  10348  lenegsq  10355  cau3lem  10374  minmax  10486  clim  10494  climshftlemg  10515  climcn1  10521  climcn1lem  10531  clim2iser  10549  clim2iser2  10550  iiserex  10551  iisermulc2  10552  climub  10556  climcaucn  10562  serif0  10563  dvdsval3  10580  iddvdsexp  10600  alzdvds  10635  addmodlteqALT  10640  nnehalf  10684  nno  10686  ndvdsadd  10711  divgcdnnr  10747  neggcd  10754  gcdabs  10759  bezoutlemmain  10767  bezoutlemaz  10772  bezoutlembz  10773  gcdmultiplez  10790  gcdzeq  10791  dvdssq  10800  ialgcvg  10810  ialgcvga  10813  ialgfx  10814  eucalgf  10817  eucialgcvga  10820  neglcm  10837  lcmabs  10838  lcmdvds  10841  lcmgcdeq  10845  qredeq  10858  isprm3  10880  coprm  10903  prmrp  10904  isprm6  10906  prmdvdsexpb  10908  rpexp  10912  cncongrprm  10916  sqrt2irraplemnn  10937  phibndlem  10972  phiprmpw  10978  bj-inex  11141  bj-nn0suc  11202  bj-nn0sucALT  11216
  Copyright terms: Public domain W3C validator