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  6571  1idsr  6696  addgt0sr  6703  gt0ap0  7408  mulgt1  7610  gt0div  7617  ge0div  7618  ltdiv2  7634  creur  7692  avgle1  7942  recnz  8109  qreccl  8351  xrrege0  8508  peano2fzor  8858  frecuzrdgfn  8879  frecuzrdgcl  8880  frecuzrdgsuc  8882  iseqfveq  8907  le2sq2  8982
  Copyright terms: Public domain W3C validator