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

Theorem syldan 282
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 116 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 279 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 36 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108
This theorem is referenced by:  sylan2  286  dn1dc  960  stoic2a  1429  sbcied2  3000  csbied2  3104  elpw2g  4153  pofun  4308  tfi  4577  fnbr  5313  caovlem2d  6060  caofcom  6099  fnexALT  6105  tfr1onlemres  6343  tfrcllemres  6356  tfri3  6361  ixpexgg  6715  f1domg  6751  fundmfi  6930  f1ofi  6935  archnqq  7394  nqpru  7529  ltaddpr  7574  1idsr  7745  addgt0sr  7752  suplocsrlempr  7784  gt0ap0  8560  ap0gt0  8574  mulgt1  8796  gt0div  8803  ge0div  8804  ltdiv2  8820  creur  8892  avgle1  9135  recnz  9322  qreccl  9618  xrrege0  9799  peano2fzor  10205  flqltnz  10260  flqdiv  10294  zmodcl  10317  frecuzrdgtcl  10385  frecuzrdgfunlem  10392  seq3fveq  10444  ser3mono  10451  iseqf1olemkle  10457  seq3f1olemqsumkj  10471  seq3f1olemqsumk  10472  seq3id  10481  seq3z  10484  le2sq2  10568  bcpasc  10717  fihasheqf1oi  10738  seq3coll  10793  caucvgrelemcau  10960  caucvgre  10961  r19.2uz  10973  sqrtgt0  11014  xrmaxiflemval  11229  clim2ser  11316  clim2ser2  11317  climub  11323  serf0  11331  fsumf1o  11369  fisumss  11371  fsumcl2lem  11377  fsumsplit  11386  fsum2dlemstep  11413  fisumrev2  11425  fsumlessfi  11439  telfsumo  11445  fsumparts  11449  fsumiun  11456  binom1dif  11466  isumsplit  11470  isumrpcl  11473  isumlessdc  11475  explecnv  11484  cvgratnnlemmn  11504  cvgratz  11511  cvgratgt0  11512  mertenslemi1  11514  clim2prod  11518  clim2divap  11519  fprodseq  11562  fprodf1o  11567  prodssdc  11568  fprodssdc  11569  fprodsplitdc  11575  fprodeq0  11596  fprod2dlemstep  11601  ef0lem  11639  eftlub  11669  tanval3ap  11693  dvdssubr  11817  divalgmod  11902  divgcdnn  11946  algfx  12022  eucalgcvga  12028  lcmcllem  12037  lcmneg  12044  isprm6  12117  cncongrprm  12127  phimullem  12195  pcid  12293  pcgcd  12298  pcz  12301  4sqlem9  12354  grpidd  12681  ismndd  12717  grpinvid1  12801  grpinvid2  12802  grplcan  12808  grpinvinv  12813  grpinvval2  12829  mulgass  12895  mulgpropdg  12900  ringidss  13025  isringd  13033  ringlz  13035  ringrz  13036  unitgrp  13097  0unit  13110  unitnegcl  13111  tgcl  13197  tgclb  13198  tgss2  13212  ntrss3  13256  ntridm  13259  opnssneib  13289  ssnei2  13290  innei  13296  resttopon  13304  cnpnei  13352  cnntri  13357  lmss  13379  txcnp  13404  blpnfctr  13572  mopni2  13616  bdmopn  13637  climcncf  13704  ivthdec  13755  cnplimcim  13769  dvconst  13794  dvef  13821  rpcxpneg  13961  abscxp  13968  lgscllem  14041  lgsvalmod  14053  lgsdir2  14067  cvgcmp2nlemabs  14403  trilpolemisumle  14409  trilpolemeq1  14411  trilpolemlt1  14412  nconstwlpolemgt0  14434  neapmkvlem  14437
  Copyright terms: Public domain W3C validator