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

Theorem syld3an3 1246
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 966 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 967 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1201 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
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 949
This theorem is referenced by:  syld3an1  1247  syld3an2  1248  brelrng  4740  moriotass  5726  nnncan1  7966  lediv1  8595  modqval  10065  modqvalr  10066  modqcl  10067  flqpmodeq  10068  modq0  10070  modqge0  10073  modqlt  10074  modqdiffl  10076  modqdifz  10077  modqvalp1  10084  exp3val  10263  bcval4  10466  dvdsmultr1  11458  dvdssub2  11462  divalglemeuneg  11547  ndvdsadd  11555  basgen2  12177  opnneiss  12254  cnpf2  12303  sincosq1lem  12833
  Copyright terms: Public domain W3C validator