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  969  stoic2a  1474  sbcied2  3083  csbied2  3189  elpw2g  4273  pofun  4438  tfi  4709  fnbr  5465  caovlem2d  6255  caofcom  6306  fnexALT  6313  elabreximd  6329  tfr1onlemres  6593  tfrcllemres  6606  tfri3  6611  ixpexgg  6970  f1domg  7010  fundmfi  7217  f1ofi  7223  finacn  7524  archnqq  7748  nqpru  7883  ltaddpr  7928  1idsr  8099  addgt0sr  8106  suplocsrlempr  8138  gt0ap0  8918  ap0gt0  8932  mulgt1  9157  gt0div  9164  ge0div  9165  ltdiv2  9181  creur  9253  avgle1  9499  recnz  9692  qreccl  9995  xrrege0  10180  peano2fzor  10602  flqltnz  10674  flqdiv  10710  zmodcl  10733  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  seqfveqg  10867  seq3fveq  10868  ser3mono  10876  seqsplitg  10878  seqcaopr2g  10883  iseqf1olemkle  10886  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seqf1oglem2  10909  seqf1og  10910  seq3id  10914  seq3z  10917  seqhomog  10919  le2sq2  11004  bcpasc  11156  fihasheqf1oi  11178  seq3coll  11242  wrdnval  11283  wrdsymb1  11289  lswcl  11303  ccatlid  11322  ccatass  11324  ccat1st1st  11357  lswccats1fst  11360  swrdlsw  11389  ccatswrd  11390  pfxtrcfvl  11417  pfxsuff1eqwrdeq  11419  ccatpfx  11421  pfx1  11423  pfxswrd  11426  pfxlswccat  11433  swrdccatin2  11449  pfxccatin12  11453  caucvgrelemcau  11694  caucvgre  11695  r19.2uz  11707  sqrtgt0  11748  xrmaxiflemval  11964  clim2ser  12051  clim2ser2  12052  climub  12058  serf0  12066  fsumf1o  12105  fisumss  12107  fsumcl2lem  12113  fsumsplit  12122  fsum2dlemstep  12149  fisumrev2  12161  fsumlessfi  12175  telfsumo  12181  fsumparts  12185  fsumiun  12192  binom1dif  12202  isumsplit  12206  isumrpcl  12209  isumlessdc  12211  explecnv  12220  cvgratnnlemmn  12240  cvgratz  12247  cvgratgt0  12248  mertenslemi1  12250  clim2prod  12254  clim2divap  12255  fprodseq  12298  fprodf1o  12303  prodssdc  12304  fprodssdc  12305  fprodsplitdc  12311  fprodeq0  12332  fprod2dlemstep  12337  ef0lem  12375  eftlub  12405  tanval3ap  12429  dvdssubr  12554  divalgmod  12642  bitsdc  12662  bitsp1  12666  divgcdnn  12700  algfx  12778  eucalgcvga  12784  lcmcllem  12793  lcmneg  12800  isprm6  12873  cncongrprm  12883  phimullem  12951  pcid  13051  pcgcd  13056  pcz  13059  4sqlem9  13113  4sqlem15  13132  4sqlem16  13133  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemsel1i  13204  ballotfilemsima  13207  ballotfilemfrceq  13220  imasex  13573  grpidd  13650  gsumress  13662  ismndd  13702  subsubm  13742  grpinvid1  13811  grpinvid2  13812  grplcan  13821  grpinvinv  13826  grpinvval2  13842  mulgass  13916  mulgpropdg  13921  subginv  13938  subgmulg  13945  issubg2m  13946  issubg4m  13950  subsubg  13954  eqger  13981  qusinv  13993  resghm  14017  conjsubgen  14035  rngrz  14189  isrngd  14196  ringidss  14276  isringd  14288  ringlz  14290  ringrz  14291  unitgrp  14365  0unit  14378  unitnegcl  14379  dvrass  14388  dvreq1  14391  dvrdir  14392  ringinvdv  14394  invrpropdg  14398  rhmunitinv  14427  issubrng2  14460  subsubrng  14464  subrg1  14481  issubrg2  14491  subsubrg  14495  lmod0vs  14599  lmodvs0  14600  lmodvneg1  14608  islss3  14657  lspsnsubg  14674  lspid  14675  lspssv  14676  lspidm  14679  lspsnneg  14698  sraval  14715  qus1  14804  zringmulg  14876  mulgrhm  14887  znidom  14935  tgcl  15059  tgclb  15060  tgss2  15074  ntrss3  15118  ntridm  15121  opnssneib  15151  ssnei2  15152  innei  15158  resttopon  15166  cnpnei  15214  cnntri  15219  lmss  15241  txcnp  15266  blpnfctr  15434  mopni2  15478  bdmopn  15499  climcncf  15579  ivthdec  15639  cnplimcim  15662  dvconst  15689  dvconstre  15691  dvef  15722  plymullem  15745  plycoeid3  15752  rpcxpneg  15902  abscxp  15910  sgmmul  15994  lgscllem  16010  lgsvalmod  16022  lgsdir2  16036  lgsquadlem2  16081  lgsquad2lem2  16085  upgredg  16269  usgruspgrben  16311  usgredg3  16339  cvgcmp2nlemabs  16956  trilpolemisumle  16962  trilpolemeq1  16964  trilpolemlt1  16965  nconstwlpolemgt0  16989  neapmkvlem  16992