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	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
syldan.2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syldan	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem syldan

Step	Hyp	Ref	Expression
1		syldan.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		syldan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
3	2	expcom 116	. . 3 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	adantrd 279	. 2 ⊢ (𝜒 → ((𝜑 ∧ 𝜓) → 𝜃))
5	1, 4	mpcom 36	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

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  966  stoic2a  1471  sbcied2  3066  csbied2  3172  elpw2g  4240  pofun  4403  tfi  4674  fnbr  5425  caovlem2d  6204  caofcom  6255  fnexALT  6262  tfr1onlemres  6501  tfrcllemres  6514  tfri3  6519  ixpexgg  6877  f1domg  6917  fundmfi  7112  f1ofi  7118  finacn  7394  archnqq  7612  nqpru  7747  ltaddpr  7792  1idsr  7963  addgt0sr  7970  suplocsrlempr  8002  gt0ap0  8781  ap0gt0  8795  mulgt1  9018  gt0div  9025  ge0div  9026  ltdiv2  9042  creur  9114  avgle1  9360  recnz  9548  qreccl  9845  xrrege0  10029  peano2fzor  10446  flqltnz  10515  flqdiv  10551  zmodcl  10574  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  seqfveqg  10708  seq3fveq  10709  ser3mono  10717  seqsplitg  10719  seqcaopr2g  10724  iseqf1olemkle  10727  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seqf1oglem2  10750  seqf1og  10751  seq3id  10755  seq3z  10758  seqhomog  10760  le2sq2  10845  bcpasc  10996  fihasheqf1oi  11017  seq3coll  11072  wrdnval  11110  wrdsymb1  11116  lswcl  11130  ccatlid  11149  ccatass  11151  ccat1st1st  11180  lswccats1fst  11183  swrdlsw  11209  ccatswrd  11210  pfxtrcfvl  11237  pfxsuff1eqwrdeq  11239  ccatpfx  11241  pfx1  11243  pfxswrd  11246  pfxlswccat  11253  swrdccatin2  11269  pfxccatin12  11273  caucvgrelemcau  11499  caucvgre  11500  r19.2uz  11512  sqrtgt0  11553  xrmaxiflemval  11769  clim2ser  11856  clim2ser2  11857  climub  11863  serf0  11871  fsumf1o  11909  fisumss  11911  fsumcl2lem  11917  fsumsplit  11926  fsum2dlemstep  11953  fisumrev2  11965  fsumlessfi  11979  telfsumo  11985  fsumparts  11989  fsumiun  11996  binom1dif  12006  isumsplit  12010  isumrpcl  12013  isumlessdc  12015  explecnv  12024  cvgratnnlemmn  12044  cvgratz  12051  cvgratgt0  12052  mertenslemi1  12054  clim2prod  12058  clim2divap  12059  fprodseq  12102  fprodf1o  12107  prodssdc  12108  fprodssdc  12109  fprodsplitdc  12115  fprodeq0  12136  fprod2dlemstep  12141  ef0lem  12179  eftlub  12209  tanval3ap  12233  dvdssubr  12358  divalgmod  12446  bitsdc  12466  bitsp1  12470  divgcdnn  12504  algfx  12582  eucalgcvga  12588  lcmcllem  12597  lcmneg  12604  isprm6  12677  cncongrprm  12687  phimullem  12755  pcid  12855  pcgcd  12860  pcz  12863  4sqlem9  12917  4sqlem15  12936  4sqlem16  12937  imasex  13346  grpidd  13424  gsumress  13436  ismndd  13478  subsubm  13524  grpinvid1  13593  grpinvid2  13594  grplcan  13603  grpinvinv  13608  grpinvval2  13624  mulgass  13704  mulgpropdg  13709  subginv  13726  subgmulg  13733  issubg2m  13734  issubg4m  13738  subsubg  13742  eqger  13769  qusinv  13781  resghm  13805  conjsubgen  13823  rngrz  13917  isrngd  13924  ringidss  14000  isringd  14012  ringlz  14014  ringrz  14015  unitgrp  14088  0unit  14101  unitnegcl  14102  dvrass  14111  dvreq1  14114  dvrdir  14115  ringinvdv  14117  invrpropdg  14121  rhmunitinv  14150  issubrng2  14182  subsubrng  14186  subrg1  14203  issubrg2  14213  subsubrg  14217  lmod0vs  14293  lmodvs0  14294  lmodvneg1  14302  islss3  14351  lspsnsubg  14368  lspid  14369  lspssv  14370  lspidm  14373  lspsnneg  14392  sraval  14409  qus1  14498  zringmulg  14570  mulgrhm  14581  znidom  14629  tgcl  14746  tgclb  14747  tgss2  14761  ntrss3  14805  ntridm  14808  opnssneib  14838  ssnei2  14839  innei  14845  resttopon  14853  cnpnei  14901  cnntri  14906  lmss  14928  txcnp  14953  blpnfctr  15121  mopni2  15165  bdmopn  15186  climcncf  15266  ivthdec  15326  cnplimcim  15349  dvconst  15376  dvconstre  15378  dvef  15409  plymullem  15432  plycoeid3  15439  rpcxpneg  15589  abscxp  15597  sgmmul  15678  lgscllem  15694  lgsvalmod  15706  lgsdir2  15720  lgsquadlem2  15765  lgsquad2lem2  15769  upgredg  15950  usgruspgrben  15992  usgredg3  16020  cvgcmp2nlemabs  16430  trilpolemisumle  16436  trilpolemeq1  16438  trilpolemlt1  16439  nconstwlpolemgt0  16462  neapmkvlem  16465