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

Theorem syldan 266
Description: A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
Hypotheses
Ref Expression
syldan.1 ((φ ψ) → χ)
syldan.2 ((φ χ) → θ)
Assertion
Ref Expression
syldan ((φ ψ) → θ)

Proof of Theorem syldan
StepHypRef Expression
1 syldan.1 . 2 ((φ ψ) → χ)
2 syldan.2 . . . 4 ((φ χ) → θ)
32expcom 109 . . 3 (χ → (φθ))
43adantrd 264 . 2 (χ → ((φ ψ) → θ))
51, 4mpcom 32 1 ((φ ψ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia3 101
This theorem is referenced by:  sylan2  270  dn1dc  855  sbcied2  2777  csbied2  2870  elpw2g  3884  pofun  4023  tfi  4232  fnbr  4927  caovlem2d  5616  grprinvlem  5618  caofcom  5657  fnexALT  5663  tfri3  5875  archnqq  6274  ltaddpr  6434  1idsr  6515  addgt0sr  6521
  Copyright terms: Public domain W3C validator