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

Theorem syld3an3 1294
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an3.1 ((𝜑𝜓𝜒) → 𝜃)
syld3an3.2 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syld3an3 ((𝜑𝜓𝜒) → 𝜏)

Proof of Theorem syld3an3
StepHypRef Expression
1 simp1 999 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 1000 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1249 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 980
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 depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  syld3an1  1295  syld3an2  1296  brelrng  4879  moriotass  5884  nnncan1  8228  lediv1  8861  modqval  10361  modqvalr  10362  modqcl  10363  flqpmodeq  10364  modq0  10366  modqge0  10369  modqlt  10370  modqdiffl  10372  modqdifz  10373  modqvalp1  10380  exp3val  10562  bcval4  10773  dvdsmultr1  11879  dvdssub2  11883  divalglemeuneg  11969  ndvdsadd  11977  grpsubf  13046  grpinvsub  13049  grpnpcan  13059  mulginvcom  13112  mulginvinv  13113  subgsubcl  13149  qussub  13201  ghmsub  13215  dvrcl  13510  unitdvcl  13511  basgen2  14066  opnneiss  14143  cnpf2  14192  sincosq1lem  14731
  Copyright terms: Public domain W3C validator