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

Theorem syldan 280
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 115 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 277 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 36 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107
This theorem is referenced by:  sylan2  284  dn1dc  929  stoic2a  1390  sbcied2  2918  csbied2  3017  elpw2g  4051  pofun  4204  tfi  4466  fnbr  5195  caovlem2d  5931  grprinvlem  5933  caofcom  5973  fnexALT  5979  tfr1onlemres  6214  tfrcllemres  6227  tfri3  6232  ixpexgg  6584  f1domg  6620  fundmfi  6794  f1ofi  6799  archnqq  7193  nqpru  7328  ltaddpr  7373  1idsr  7544  addgt0sr  7551  suplocsrlempr  7583  gt0ap0  8356  ap0gt0  8370  mulgt1  8589  gt0div  8596  ge0div  8597  ltdiv2  8613  creur  8685  avgle1  8928  recnz  9112  qreccl  9402  xrrege0  9576  peano2fzor  9977  flqltnz  10028  flqdiv  10062  zmodcl  10085  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  seq3fveq  10212  ser3mono  10219  iseqf1olemkle  10225  seq3f1olemqsumkj  10239  seq3f1olemqsumk  10240  seq3id  10249  seq3z  10252  le2sq2  10336  bcpasc  10480  fihasheqf1oi  10502  seq3coll  10553  caucvgrelemcau  10720  caucvgre  10721  r19.2uz  10733  sqrtgt0  10774  xrmaxiflemval  10987  clim2ser  11074  clim2ser2  11075  climub  11081  serf0  11089  fsumf1o  11127  fisumss  11129  fsumcl2lem  11135  fsumsplit  11144  fsum2dlemstep  11171  fisumrev2  11183  fsumlessfi  11197  telfsumo  11203  fsumparts  11207  fsumiun  11214  binom1dif  11224  isumsplit  11228  isumrpcl  11231  isumlessdc  11233  explecnv  11242  cvgratnnlemmn  11262  cvgratz  11269  cvgratgt0  11270  mertenslemi1  11272  ef0lem  11293  eftlub  11323  tanval3ap  11348  dvdssubr  11466  divalgmod  11551  divgcdnn  11590  algfx  11660  eucalgcvga  11666  lcmcllem  11675  lcmneg  11682  isprm6  11752  cncongrprm  11762  phimullem  11828  tgcl  12160  tgclb  12161  tgss2  12175  ntrss3  12219  ntridm  12222  opnssneib  12252  ssnei2  12253  innei  12259  resttopon  12267  cnpnei  12315  cnntri  12320  lmss  12342  txcnp  12367  blpnfctr  12535  mopni2  12579  bdmopn  12600  climcncf  12667  ivthdec  12718  cnplimcim  12732  dvconst  12757  dvef  12783  cvgcmp2nlemabs  13154  trilpolemisumle  13158  trilpolemeq1  13160  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator