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

Theorem syldan 270
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  |-  ( (
ph  /\  ps )  ->  ch )
syldan.2  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
syldan  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem syldan
StepHypRef Expression
1 syldan.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 syldan.2 . . . 4  |-  ( (
ph  /\  ch )  ->  th )
32expcom 113 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 268 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 36 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia3 105
This theorem is referenced by:  sylan2  274  dn1dc  878  stoic2a  1334  sbcied2  2823  csbied2  2921  elpw2g  3938  pofun  4077  tfi  4333  fnbr  5029  caovlem2d  5721  grprinvlem  5723  caofcom  5762  fnexALT  5768  tfri3  5984  f1domg  6269  archnqq  6573  nqpru  6708  ltaddpr  6753  1idsr  6911  addgt0sr  6918  gt0ap0  7690  ap0gt0  7703  mulgt1  7904  gt0div  7911  ge0div  7912  ltdiv2  7928  creur  7987  avgle1  8222  recnz  8391  qreccl  8674  xrrege0  8839  peano2fzor  9190  flqltnz  9237  flqdiv  9271  zmodcl  9294  frecuzrdgfn  9362  frecuzrdgcl  9363  frecuzrdgsuc  9365  iseqfveq  9394  isermono  9401  iseqsplit  9402  iseqid  9411  iseqz  9413  le2sq2  9495  bcpasc  9634  caucvgrelemcau  9807  caucvgre  9808  r19.2uz  9820  sqrtgt0  9861  clim2iser  10088  clim2iser2  10089  climub  10095  serif0  10102  dvdssubr  10153  divalgmod  10239  ialgfx  10274
  Copyright terms: Public domain W3C validator