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  8917  ap0gt0  8931  mulgt1  9154  gt0div  9161  ge0div  9162  ltdiv2  9178  creur  9250  avgle1  9496  recnz  9689  qreccl  9992  xrrege0  10177  peano2fzor  10599  flqltnz  10671  flqdiv  10707  zmodcl  10730  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  seqfveqg  10864  seq3fveq  10865  ser3mono  10873  seqsplitg  10875  seqcaopr2g  10880  iseqf1olemkle  10883  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seqf1oglem2  10906  seqf1og  10907  seq3id  10911  seq3z  10914  seqhomog  10916  le2sq2  11001  bcpasc  11153  fihasheqf1oi  11175  seq3coll  11239  wrdnval  11280  wrdsymb1  11286  lswcl  11300  ccatlid  11319  ccatass  11321  ccat1st1st  11354  lswccats1fst  11357  swrdlsw  11386  ccatswrd  11387  pfxtrcfvl  11414  pfxsuff1eqwrdeq  11416  ccatpfx  11418  pfx1  11420  pfxswrd  11423  pfxlswccat  11430  swrdccatin2  11446  pfxccatin12  11450  caucvgrelemcau  11690  caucvgre  11691  r19.2uz  11703  sqrtgt0  11744  xrmaxiflemval  11960  clim2ser  12047  clim2ser2  12048  climub  12054  serf0  12062  fsumf1o  12101  fisumss  12103  fsumcl2lem  12109  fsumsplit  12118  fsum2dlemstep  12145  fisumrev2  12157  fsumlessfi  12171  telfsumo  12177  fsumparts  12181  fsumiun  12188  binom1dif  12198  isumsplit  12202  isumrpcl  12205  isumlessdc  12207  explecnv  12216  cvgratnnlemmn  12236  cvgratz  12243  cvgratgt0  12244  mertenslemi1  12246  clim2prod  12250  clim2divap  12251  fprodseq  12294  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodsplitdc  12307  fprodeq0  12328  fprod2dlemstep  12333  ef0lem  12371  eftlub  12401  tanval3ap  12425  dvdssubr  12550  divalgmod  12638  bitsdc  12658  bitsp1  12662  divgcdnn  12696  algfx  12774  eucalgcvga  12780  lcmcllem  12789  lcmneg  12796  isprm6  12869  cncongrprm  12879  phimullem  12947  pcid  13047  pcgcd  13052  pcz  13055  4sqlem9  13109  4sqlem15  13128  4sqlem16  13129  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsel1i  13200  ballotfilemsima  13203  ballotfilemfrceq  13216  imasex  13602  grpidd  13680  gsumress  13692  ismndd  13734  subsubm  13780  grpinvid1  13849  grpinvid2  13850  grplcan  13859  grpinvinv  13864  grpinvval2  13880  mulgass  13960  mulgpropdg  13965  subginv  13982  subgmulg  13989  issubg2m  13990  issubg4m  13994  subsubg  13998  eqger  14025  qusinv  14037  resghm  14061  conjsubgen  14079  rngrz  14174  isrngd  14181  ringidss  14257  isringd  14269  ringlz  14271  ringrz  14272  unitgrp  14346  0unit  14359  unitnegcl  14360  dvrass  14369  dvreq1  14372  dvrdir  14373  ringinvdv  14375  invrpropdg  14379  rhmunitinv  14408  issubrng2  14441  subsubrng  14445  subrg1  14462  issubrg2  14472  subsubrg  14476  lmod0vs  14581  lmodvs0  14582  lmodvneg1  14590  islss3  14639  lspsnsubg  14656  lspid  14657  lspssv  14658  lspidm  14661  lspsnneg  14680  sraval  14697  qus1  14786  zringmulg  14858  mulgrhm  14869  znidom  14917  tgcl  15041  tgclb  15042  tgss2  15056  ntrss3  15100  ntridm  15103  opnssneib  15133  ssnei2  15134  innei  15140  resttopon  15148  cnpnei  15196  cnntri  15201  lmss  15223  txcnp  15248  blpnfctr  15416  mopni2  15460  bdmopn  15481  climcncf  15561  ivthdec  15621  cnplimcim  15644  dvconst  15671  dvconstre  15673  dvef  15704  plymullem  15727  plycoeid3  15734  rpcxpneg  15884  abscxp  15892  sgmmul  15976  lgscllem  15992  lgsvalmod  16004  lgsdir2  16018  lgsquadlem2  16063  lgsquad2lem2  16067  upgredg  16251  usgruspgrben  16293  usgredg3  16321  cvgcmp2nlemabs  16928  trilpolemisumle  16934  trilpolemeq1  16936  trilpolemlt1  16937  nconstwlpolemgt0  16962  neapmkvlem  16965