Theorem syldan 278

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

Step	Hyp	Ref	Expression
1		syldan.1	. 2 |- ( ( ph /\ ps ) -> ch )
2		syldan.2	. . . 4 |- ( ( ph /\ ch ) -> th )
3	2	expcom 115	. . 3 |- ( ch -> ( ph -> th ) )
4	3	adantrd 275	. 2 |- ( ch -> ( ( ph /\ ps ) -> th ) )
5	1, 4	mpcom 36	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia3 107

This theorem is referenced by:  sylan2  282  dn1dc  925  stoic2a  1386  sbcied2  2912  csbied2  3011  elpw2g  4039  pofun  4192  tfi  4454  fnbr  5181  caovlem2d  5915  grprinvlem  5917  caofcom  5957  fnexALT  5963  tfr1onlemres  6198  tfrcllemres  6211  tfri3  6216  ixpexgg  6568  f1domg  6604  fundmfi  6776  f1ofi  6781  archnqq  7167  nqpru  7302  ltaddpr  7347  1idsr  7505  addgt0sr  7512  gt0ap0  8300  ap0gt0  8313  mulgt1  8525  gt0div  8532  ge0div  8533  ltdiv2  8549  creur  8621  avgle1  8858  recnz  9042  qreccl  9330  xrrege0  9495  peano2fzor  9896  flqltnz  9947  flqdiv  9981  zmodcl  10004  frecuzrdgtcl  10072  frecuzrdgfunlem  10079  seq3fveq  10131  ser3mono  10138  iseqf1olemkle  10144  seq3f1olemqsumkj  10158  seq3f1olemqsumk  10159  seq3id  10168  seq3z  10171  le2sq2  10255  bcpasc  10399  fihasheqf1oi  10421  seq3coll  10472  caucvgrelemcau  10638  caucvgre  10639  r19.2uz  10651  sqrtgt0  10692  xrmaxiflemval  10905  clim2ser  10992  clim2ser2  10993  climub  10999  serf0  11007  fsumf1o  11045  fisumss  11047  fsumcl2lem  11053  fsumsplit  11062  fsum2dlemstep  11089  fisumrev2  11101  fsumlessfi  11115  telfsumo  11121  fsumparts  11125  fsumiun  11132  binom1dif  11142  isumsplit  11146  isumrpcl  11149  isumlessdc  11151  explecnv  11160  cvgratnnlemmn  11180  cvgratz  11187  cvgratgt0  11188  mertenslemi1  11190  ef0lem  11211  eftlub  11241  tanval3ap  11266  dvdssubr  11381  divalgmod  11466  divgcdnn  11505  algfx  11573  eucalgcvga  11579  lcmcllem  11588  lcmneg  11595  isprm6  11665  cncongrprm  11675  phimullem  11740  tgcl  12070  tgclb  12071  tgss2  12085  ntrss3  12129  ntridm  12132  opnssneib  12162  ssnei2  12163  innei  12169  resttopon  12177  cnpnei  12224  cnntri  12229  lmss  12251  txcnp  12276  blpnfctr  12422  mopni2  12466  bdmopn  12487  climcncf  12551  cnplimcim  12586  dvconst  12610  cvgcmp2nlemabs  12908  trilpolemisumle  12912  trilpolemeq1  12914  trilpolemlt1  12915