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

Theorem syld3an3 1262
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 982 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 983 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1217 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  syld3an1  1263  syld3an2  1264  brelrng  4778  moriotass  5766  nnncan1  8022  lediv1  8651  modqval  10128  modqvalr  10129  modqcl  10130  flqpmodeq  10131  modq0  10133  modqge0  10136  modqlt  10137  modqdiffl  10139  modqdifz  10140  modqvalp1  10147  exp3val  10326  bcval4  10530  dvdsmultr1  11567  dvdssub2  11571  divalglemeuneg  11656  ndvdsadd  11664  basgen2  12289  opnneiss  12366  cnpf2  12415  sincosq1lem  12954
  Copyright terms: Public domain W3C validator