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

Theorem syld3an3 1217
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 941 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 942 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1172 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 922
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 depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  syld3an1  1218  syld3an2  1219  brelrng  4634  moriotass  5597  nnncan1  7662  lediv1  8265  modqval  9659  modqvalr  9660  modqcl  9661  flqpmodeq  9662  modq0  9664  modqge0  9667  modqlt  9668  modqdiffl  9670  modqdifz  9671  modqvalp1  9678  expival  9855  bcval4  10056  dvdsmultr1  10709  dvdssub2  10713  divalglemeuneg  10798  ndvdsadd  10806
  Copyright terms: Public domain W3C validator