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  973  stoic2a  1478  sbcied2  3089  csbied2  3195  elpw2g  4290  pofun  4455  tfi  4727  fnbr  5483  caovlem2d  6276  caofcom  6327  fnexALT  6334  elabreximd  6350  tfr1onlemres  6614  tfrcllemres  6627  tfri3  6632  ixpexgg  6998  f1domg  7038  fundmfi  7245  f1ofi  7251  finacn  7554  archnqq  7778  nqpru  7913  ltaddpr  7958  1idsr  8129  addgt0sr  8136  suplocsrlempr  8168  gt0ap0  8948  ap0gt0  8962  mulgt1  9187  gt0div  9194  ge0div  9195  ltdiv2  9211  creur  9283  avgle1  9529  recnz  9722  qreccl  10025  xrrege0  10210  peano2fzor  10633  flqltnz  10705  flqdiv  10741  zmodcl  10764  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  seqfveqg  10898  seq3fveq  10899  ser3mono  10907  seqsplitg  10909  seqcaopr2g  10914  iseqf1olemkle  10917  seq3f1olemqsumkj  10931  seq3f1olemqsumk  10932  seqf1oglem2  10940  seqf1og  10941  seq3id  10945  seq3z  10948  seqhomog  10950  le2sq2  11035  bcpasc  11187  fihasheqf1oi  11209  seq3coll  11277  wrdnval  11318  wrdsymb1  11324  lswcl  11338  ccatlid  11357  ccatass  11359  ccat1st1st  11392  lswccats1fst  11395  swrdlsw  11424  ccatswrd  11425  pfxtrcfvl  11452  pfxsuff1eqwrdeq  11454  ccatpfx  11456  pfx1  11458  pfxswrd  11461  pfxlswccat  11468  swrdccatin2  11484  pfxccatin12  11488  caucvgrelemcau  11729  caucvgre  11730  r19.2uz  11742  sqrtgt0  11783  xrmaxiflemval  11999  clim2ser  12086  clim2ser2  12087  climub  12093  serf0  12101  fsumf1o  12140  fisumss  12142  fsumcl2lem  12148  fsumsplit  12157  fsum2dlemstep  12184  fisumrev2  12196  fsumlessfi  12210  telfsumo  12216  fsumparts  12220  fsumiun  12227  binom1dif  12237  isumsplit  12241  isumrpcl  12244  isumlessdc  12246  explecnv  12255  cvgratnnlemmn  12275  cvgratz  12282  cvgratgt0  12283  mertenslemi1  12285  clim2prod  12289  clim2divap  12290  fprodseq  12333  fprodf1o  12338  prodssdc  12339  fprodssdc  12340  fprodsplitdc  12346  fprodeq0  12367  fprod2dlemstep  12372  ef0lem  12410  eftlub  12440  tanval3ap  12464  dvdssubr  12589  divalgmod  12677  bitsdc  12697  bitsp1  12701  divgcdnn  12735  algfx  12813  eucalgcvga  12819  lcmcllem  12828  lcmneg  12835  isprm6  12908  cncongrprm  12918  phimullem  12986  pcid  13086  pcgcd  13091  pcz  13094  4sqlem9  13148  4sqlem15  13167  4sqlem16  13168  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemsel1i  13239  ballotfilemsima  13242  ballotfilemfrceq  13255  imasex  13609  grpidd  13686  gzsumress  13695  ismndd  13733  subsubm  13773  grpinvid1  13840  grpinvid2  13841  grplcan  13850  grpinvinv  13855  grpinvval2  13871  mulgass  13945  mulgpropdg  13950  subginv  13967  subgmulg  13974  issubg2m  13975  issubg4m  13979  subsubg  13983  eqger  14010  qusinv  14022  resghm  14046  conjsubgen  14064  rngrz  14228  isrngd  14235  ringidss  14317  isringd  14329  ringlz  14331  ringrz  14332  unitgrp  14406  0unit  14419  unitnegcl  14420  dvrass  14429  dvreq1  14432  dvrdir  14433  ringinvdv  14435  invrpropdg  14439  rhmunitinv  14468  issubrng2  14501  subsubrng  14505  subrg1  14522  issubrg2  14532  subsubrg  14536  lmod0vs  14641  lmodvs0  14642  lmodvneg1  14650  islss3  14699  lspsnsubg  14716  lspid  14717  lspssv  14718  lspidm  14721  lspsnneg  14740  sraval  14757  qus1  14846  zringmulg  14916  mulgrhm  14927  znidom  14975  issubassa3  14995  tgcl  15148  tgclb  15149  tgss2  15163  ntrss3  15207  ntridm  15210  opnssneib  15240  ssnei2  15241  innei  15247  resttopon  15255  cnpnei  15303  cnntri  15308  lmss  15330  txcnp  15355  blpnfctr  15523  mopni2  15567  bdmopn  15588  climcncf  15668  ivthdec  15728  cnplimcim  15751  dvconst  15778  dvconstre  15780  dvef  15811  plymullem  15834  plycoeid3  15841  rpcxpneg  15992  abscxp  16000  log2tlbndlog2  16065  birthdaylem2  16071  sgmmul  16093  lgscllem  16109  lgsvalmod  16121  lgsdir2  16135  lgsquadlem2  16180  lgsquad2lem2  16184  upgredg  16368  usgruspgrben  16410  usgredg3  16438  cvgcmp2nlemabs  17055  trilpolemisumle  17061  trilpolemeq1  17063  trilpolemlt1  17064  nconstwlpolemgt0  17088  neapmkvlem  17091