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

Theorem sylan2 270
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
Hypotheses
Ref Expression
sylan2.1 (φχ)
sylan2.2 ((ψ χ) → θ)
Assertion
Ref Expression
sylan2 ((ψ φ) → θ)

Proof of Theorem sylan2
StepHypRef Expression
1 sylan2.1 . . 3 (φχ)
21adantl 262 . 2 ((ψ φ) → χ)
3 sylan2.2 . 2 ((ψ χ) → θ)
42, 3syldan 266 1 ((ψ φ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  sylan2b  271  sylan2br  272  syl2an  273  sylanr1  384  sylanr2  385  mpanr2  414  adantrl  447  adantrr  448  ancom2s  485  3adantr1  1047  3adantr2  1048  3adantr3  1049  syl3anr1  1170  syl3anr3  1172  dfbi3dc  1269  xordidc  1271  elabgt  2655  sbciegft  2764  csbtt  2833  csbnestgf  2869  copsex2t  3948  pofun  4015  onsucmin  4173  onsucelsucr  4174  onsucsssucr  4175  ordsucunielexmid  4191  ordsuc  4216  nlimsucg  4217  elnn  4246  xpsspw  4368  elxp4  4726  elxp5  4727  funimass2  4894  imain  4898  funimaexg  4900  dff1o2  5047  resdif  5064  funbrfv  5128  fvelimab  5145  eqfnfv2  5182  fvimacnvi  5197  ffvresb  5244  fnressn  5265  fmptapd  5270  fnex  5299  rexima  5310  ralima  5311  f1elima  5328  fnotovb  5462  mpt2eq12  5479  fovrn  5557  fnovrn  5562  ofrfval  5634  fnofval  5635  cofunexg  5652  cofunex2g  5653  mpt2exxg  5747  mpt2exg  5748  f1o2ndf1  5763  smodm2  5823  tfrlem9  5848  tfrlemibxssdm  5853  tfri3  5866  rdgruledefgg  5873  frecsuclem1  5894  oav2  5949  oasuc  5950  omv2  5951  onasuc  5952  omsuc  5957  onmsuc  5958  nnaass  5970  nndi  5971  nndir  5975  nnaword  5986  ecelqsg  6061  iinerm  6080  ecovass  6117  ecoviass  6118  ecovdi  6119  ecovidi  6120  addclpi  6176  addasspig  6179  mulasspig  6181  distrpig  6182  mulcanpig  6184  nnppipi  6191  enqdc1  6210  addassnqg  6230  ltbtwnnqq  6261  prarloclemarch  6264  prarloclemarch2  6265  enq0sym  6276  enq0ref  6277  addclnq0  6295  nqpnq0nq  6297  nnanq0  6302  distrnq0  6303  addassnq0lemcl  6305  addassnq0  6306  distnq0r  6307  prarloclemlt  6336  genpassl  6368  genpassu  6369  genpassg  6370  addcomprg  6406  mulcomprg  6408  distrlem1prl  6410  distrlem1pru  6411  1idprl  6418  1idpru  6419  recexprlemdisj  6454  recexprlem1ssl  6457  ax1rid  6569  le2tri3i  6729  add4  6775  cnegexlem1  6789  cnegexlem3  6791  cnegex  6792  subadd  6817  addsub  6825  addsubeq4  6829  negdi  6870  renegcl  6874  resubcl  6877  subdi  6984  mulneg2  6995  mul2neg  6997  submul2  6998  ltnegcon2  7060  lenegcon2  7063  lesub0  7075  cru  7192  recextlem1  7220  recexap  7222  div12ap  7261  divnegap  7271  letrp1  7400  peano2nn  7512  nndivre  7535  nnsub  7538  nndivtr  7541  nn0addge1  7805  nn0addge2  7806  zaddcl  7861  zsubcl  7862  zltnle  7866  zrevaddcl  7869  zleltp1  7873  zltlem1  7875  zdiv  7896  peano2uz2  7913  uzind  7917  qaddcl  8056  qsubcl  8059  qreccl  8061  qdivcl  8062  qrevaddcl  8063  irradd  8065  irrmul  8066  rerpdivcl  8097  xrre  8212  elioc2  8284  icoshft  8337  iccdil  8345  bj-inex  8480  findset  8521  bj-findis  8551
  Copyright terms: Public domain W3C validator