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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem is used by:  sylan2  286  dn1dc  973  stoic2a  1478  sbcied2  3089  csbied2  3195  elpw2g  4292  pofun  4457  tfi  4729  fnbr  5485  caovlem2d  6282  caofcom  6333  fnexALT  6340  elabreximd  6356  tfr1onlemres  6620  tfrcllemres  6633  tfri3  6638  ixpexgg  7004  f1domg  7044  fundmfi  7251  f1ofi  7257  finacn  7560  archnqq  7784  nqpru  7919  ltaddpr  7964  1idsr  8135  addgt0sr  8142  suplocsrlempr  8174  gt0ap0  8955  ap0gt0  8969  mulgt1  9194  gt0div  9201  ge0div  9202  ltdiv2  9218  creur  9290  avgle1  9548  recnz  9741  qreccl  10044  xrrege0  10229  peano2fzor  10652  flqltnz  10724  flqdiv  10760  zmodcl  10783  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  seqfveqg  10917  seq3fveq  10918  ser3mono  10926  seqsplitg  10928  seqcaopr2g  10933  iseqf1olemkle  10936  seq3f1olemqsumkj  10950  seq3f1olemqsumk  10951  seqf1oglem2  10959  seqf1og  10960  seq3id  10964  seq3z  10967  seqhomog  10969  le2sq2  11054  bcpasc  11206  fihasheqf1oi  11228  seq3coll  11296  wrdnval  11337  wrdsymb1  11343  lswcl  11357  ccatlid  11376  ccatass  11378  ccat1st1st  11411  lswccats1fst  11414  swrdlsw  11443  ccatswrd  11444  pfxtrcfvl  11471  pfxsuff1eqwrdeq  11473  ccatpfx  11475  pfx1  11477  pfxswrd  11480  pfxlswccat  11487  swrdccatin2  11503  pfxccatin12  11507  caucvgrelemcau  11748  caucvgre  11749  r19.2uz  11761  sqrtgt0  11802  xrmaxiflemval  12018  clim2ser  12105  clim2ser2  12106  climub  12112  serf0  12120  fsumf1o  12159  fisumss  12161  fsumcl2lem  12167  fsumsplit  12176  fsum2dlemstep  12203  fisumrev2  12215  fsumlessfi  12229  telfsumo  12235  fsumparts  12239  fsumiun  12246  binom1dif  12256  isumsplit  12260  isumrpcl  12263  isumlessdc  12265  explecnv  12274  cvgratnnlemmn  12294  cvgratz  12301  cvgratgt0  12302  mertenslemi1  12304  clim2prod  12308  clim2divap  12309  fprodseq  12352  fprodf1o  12357  prodssdc  12358  fprodssdc  12359  fprodsplitdc  12365  fprodeq0  12386  fprod2dlemstep  12391  ef0lem  12429  eftlub  12459  tanval3ap  12483  dvdssubr  12608  divalgmod  12696  bitsdc  12716  bitsp1  12720  divgcdnn  12754  algfx  12832  eucalgcvga  12838  lcmcllem  12847  lcmneg  12854  isprm6  12927  cncongrprm  12937  phimullem  13005  pcid  13105  pcgcd  13110  pcz  13113  4sqlem9  13167  4sqlem15  13186  4sqlem16  13187  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemsel1i  13258  ballotfilemsima  13261  ballotfilemfrceq  13274  imasex  13628  grpidd  13705  gzsumress  13714  ismndd  13752  subsubm  13792  grpinvid1  13859  grpinvid2  13860  grplcan  13869  grpinvinv  13874  grpinvval2  13890  mulgass  13964  mulgpropdg  13969  subginv  13986  subgmulg  13993  issubg2m  13994  issubg4m  13998  subsubg  14002  eqger  14029  qusinv  14041  resghm  14065  conjsubgen  14083  rngrz  14247  isrngd  14254  ringidss  14336  isringd  14348  ringlz  14350  ringrz  14351  unitgrp  14425  0unit  14438  unitnegcl  14439  dvrass  14448  dvreq1  14451  dvrdir  14452  ringinvdv  14454  invrpropdg  14458  rhmunitinv  14487  issubrng2  14520  subsubrng  14524  subrg1  14541  issubrg2  14551  subsubrg  14555  lmod0vs  14660  lmodvs0  14661  lmodvneg1  14669  islss3  14718  lspsnsubg  14735  lspid  14736  lspssv  14737  lspidm  14740  lspsnneg  14759  sraval  14776  qus1  14865  zringmulg  14935  mulgrhm  14946  znidom  14994  issubassa3  15014  tgcl  15167  tgclb  15168  tgss2  15182  ntrss3  15226  ntridm  15229  opnssneib  15259  ssnei2  15260  innei  15266  resttopon  15274  cnpnei  15322  cnntri  15327  lmss  15349  txcnp  15374  blpnfctr  15542  mopni2  15586  bdmopn  15607  climcncf  15687  ivthdec  15747  cnplimcim  15770  dvconst  15797  dvconstre  15799  dvef  15830  plymullem  15853  plycoeid3  15860  rpcxpneg  16015  abscxp  16023  log2tlbndlog2  16088  birthdaylem2  16094  sgmmul  16116  lgscllem  16138  lgsvalmod  16150  lgsdir2  16164  lgsquadlem2  16209  lgsquad2lem2  16213  upgredg  16397  usgruspgrben  16439  usgredg3  16467  cvgcmp2nlemabs  17093  trilpolemisumle  17099  trilpolemeq1  17101  trilpolemlt1  17102  nconstwlpolemgt0  17126  neapmkvlem  17129