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  866  stoic2a  1315  sbcied2  2794  csbied2  2887  elpw2g  3901  pofun  4040  tfi  4248  fnbr  4944  caovlem2d  5635  grprinvlem  5637  caofcom  5676  fnexALT  5682  tfri3  5894  f1domg  6174  archnqq  6400  ltaddpr  6569  1idsr  6656  addgt0sr  6663  gt0ap0  7368  mulgt1  7570  gt0div  7577  ge0div  7578  ltdiv2  7594  creur  7652  avgle1  7902  recnz  8069  qreccl  8311  xrrege0  8468  peano2fzor  8818  frecuzrdgfn  8839  frecuzrdgcl  8840  frecuzrdgsuc  8842  iseqfveq  8867  le2sq2  8942
  Copyright terms: Public domain W3C validator