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

Theorem 3syl 17
Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3syl.1 (𝜑𝜓)
3syl.2 (𝜓𝜒)
3syl.3 (𝜒𝜃)
Assertion
Ref Expression
3syl (𝜑𝜃)

Proof of Theorem 3syl
StepHypRef Expression
1 3syl.1 . . 3 (𝜑𝜓)
2 3syl.2 . . 3 (𝜓𝜒)
31, 2syl 14 . 2 (𝜑𝜒)
4 3syl.3 . 2 (𝜒𝜃)
53, 4syl 14 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  4syl  18  simpl2im  378  hbim  1478  19.9hd  1593  equsexd  1659  sbcof2  1733  aev  1735  sbequi  1762  nfsbd  1894  mo2n  1971  eupickb  2024  r19.29af2  2502  spc2gv  2699  spc3gv  2701  eqvincg  2729  sbcco3g  2970  snelpwi  4003  opth1  4027  frind  4143  onin  4177  reusv1  4244  xpexg  4510  dmexg  4655  rnexg  4656  relfld  4913  funimaexglem  5050  funimaexg  5051  fabexg  5146  nfvres  5282  funimass4  5300  funconstss  5362  f1oresrab  5405  resfunexg  5458  f1eqcocnv  5510  isores1  5533  isoini  5536  isose  5539  isopolem  5540  isosolem  5542  eusvobj2  5577  acexmidlemcase  5586  oprabid  5616  offval  5798  resfunexgALT  5816  offval3  5840  1stvalg  5848  2ndvalg  5849  1stcof  5869  2ndcof  5870  cnvf1o  5925  tposf12  5966  smores3  5990  smoiso  5999  tfr0dm  6019  tfrlemibxssdm  6024  tfrlemi14d  6030  tfrexlem  6031  tfr1onlemssrecs  6036  tfr1onlemsucfn  6037  tfr1onlemsucaccv  6038  tfr1onlembxssdm  6040  tfr1onlemres  6046  tfri1dALT  6048  tfrcllemssrecs  6049  tfrcllemsucfn  6050  tfrcllemsucaccv  6051  tfrcllembxssdm  6053  tfrcllemres  6059  rdgss  6080  nnsucsssuc  6185  swoord1  6251  swoord2  6252  iinerm  6294  eroveu  6313  pmresg  6363  en1uniel  6451  fopwdom  6482  xpen  6491  ssenen  6497  isinfinf  6543  ac6sfi  6544  supubti  6601  suplubti  6602  isotilem  6608  supisolem  6610  supisoex  6611  supisoti  6612  ordiso2  6635  djur  6664  eldju1st  6669  eldju2ndl  6670  updjud  6680  djudom  6694  en2other2  6725  addclnq  6837  mulclnq  6838  1qec  6850  prarloclemarch2  6881  enq0tr  6896  addclnq0  6913  mulclnq0  6914  nq0m0r  6918  prarloclemlo  6956  prarloc  6965  genpml  6979  genpmu  6980  addnqprl  6991  addnqpru  6992  recnnpr  7010  prmuloc2  7029  1idpru  7053  ltexprlemm  7062  ltexprlemloc  7069  recexprlemm  7086  recexprlem1ssl  7095  caucvgprlemnkj  7128  caucvgprlemnbj  7129  caucvgprlemm  7130  caucvgprlemopl  7131  caucvgprlemlol  7132  caucvgprlemladdfu  7139  caucvgprlemladdrl  7140  caucvgprprlemk  7145  caucvgprprlemloccalc  7146  caucvgprprlemnkltj  7151  caucvgprprlemnjltk  7153  caucvgprprlemml  7156  caucvgprprlemmu  7157  caucvgprprlemlol  7160  caucvgprprlemexb  7169  caucvgprprlem1  7171  addclsr  7202  mulclsr  7203  prsrcl  7232  caucvgsrlemoffcau  7246  peano5nnnn  7330  mulap0r  7992  nn1suc  8335  prime  8741  zindd  8760  xrlttri3  9162  fzopth  9369  fzsuc  9376  fzpred  9377  fzp1ss  9380  fztp  9385  fseq1p1m1  9401  1fv  9440  elfzom1elp1fzo  9502  ssfzo12  9524  fzosplitsn  9533  divfl0  9592  modqid  9645  modqmuladdim  9663  frecuzrdgtcl  9708  frecuzrdgfunlem  9715  frecfzennn  9722  frecfzen2  9723  iseqvalt  9751  iseqsplit  9773  iseqid3s  9781  faclbnd  9984  faclbnd3  9986  bcm1k  10003  hashfz1  10026  focdmex  10030  hashfz  10064  hashfzp1  10067  hashfacen  10075  cjcj  10144  caucvgre  10241  r19.2uz  10253  resqrexlemgt0  10280  ltabs  10347  nn0o  10687  zsupcllemstep  10721  zsupcllemex  10722  infssuzledc  10726  gcdmultiplez  10790  dvdssq  10800  eucialg  10821  lcmgcdnn  10844  dvdsnprmd  10887  prm2orodd  10888  qnumdenbi  10950  nn0gcdsq  10958  phibnd  10973  hashdvds  10977  phimullem  10981  hashgcdlem  10983  unennn  10990  bj-inex  11141  bj-sucexg  11156  bj-peano4  11193  setindis  11205  bdsetindis  11207  bj-inf2vnlem1  11208  nnsf  11237  nninfalllemn  11240  nninfall  11242  nninfsellemeq  11248
  Copyright terms: Public domain W3C validator