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

Theorem syld3an3 1244
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 964 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 965 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1199 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  syld3an1  1245  syld3an2  1246  brelrng  4730  moriotass  5712  nnncan1  7921  lediv1  8537  modqval  9990  modqvalr  9991  modqcl  9992  flqpmodeq  9993  modq0  9995  modqge0  9998  modqlt  9999  modqdiffl  10001  modqdifz  10002  modqvalp1  10009  exp3val  10188  bcval4  10391  dvdsmultr1  11379  dvdssub2  11383  divalglemeuneg  11468  ndvdsadd  11476  basgen2  12093  opnneiss  12170  cnpf2  12218
  Copyright terms: Public domain W3C validator