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  4239  pofun  4400  tfi  4671  fnbr  5421  caovlem2d  6189  caofcom  6239  fnexALT  6246  tfr1onlemres  6485  tfrcllemres  6498  tfri3  6503  ixpexgg  6859  f1domg  6899  fundmfi  7092  f1ofi  7098  finacn  7374  archnqq  7592  nqpru  7727  ltaddpr  7772  1idsr  7943  addgt0sr  7950  suplocsrlempr  7982  gt0ap0  8761  ap0gt0  8775  mulgt1  8998  gt0div  9005  ge0div  9006  ltdiv2  9022  creur  9094  avgle1  9340  recnz  9528  qreccl  9825  xrrege0  10009  peano2fzor  10425  flqltnz  10494  flqdiv  10530  zmodcl  10553  frecuzrdgtcl  10621  frecuzrdgfunlem  10628  seqfveqg  10687  seq3fveq  10688  ser3mono  10696  seqsplitg  10698  seqcaopr2g  10703  iseqf1olemkle  10706  seq3f1olemqsumkj  10720  seq3f1olemqsumk  10721  seqf1oglem2  10729  seqf1og  10730  seq3id  10734  seq3z  10737  seqhomog  10739  le2sq2  10824  bcpasc  10975  fihasheqf1oi  10996  seq3coll  11051  wrdnval  11088  wrdsymb1  11094  lswcl  11108  ccatlid  11127  ccatass  11129  ccat1st1st  11158  lswccats1fst  11161  swrdlsw  11187  ccatswrd  11188  pfxtrcfvl  11215  pfxsuff1eqwrdeq  11217  ccatpfx  11219  pfx1  11221  pfxswrd  11224  pfxlswccat  11231  swrdccatin2  11247  pfxccatin12  11251  caucvgrelemcau  11477  caucvgre  11478  r19.2uz  11490  sqrtgt0  11531  xrmaxiflemval  11747  clim2ser  11834  clim2ser2  11835  climub  11841  serf0  11849  fsumf1o  11887  fisumss  11889  fsumcl2lem  11895  fsumsplit  11904  fsum2dlemstep  11931  fisumrev2  11943  fsumlessfi  11957  telfsumo  11963  fsumparts  11967  fsumiun  11974  binom1dif  11984  isumsplit  11988  isumrpcl  11991  isumlessdc  11993  explecnv  12002  cvgratnnlemmn  12022  cvgratz  12029  cvgratgt0  12030  mertenslemi1  12032  clim2prod  12036  clim2divap  12037  fprodseq  12080  fprodf1o  12085  prodssdc  12086  fprodssdc  12087  fprodsplitdc  12093  fprodeq0  12114  fprod2dlemstep  12119  ef0lem  12157  eftlub  12187  tanval3ap  12211  dvdssubr  12336  divalgmod  12424  bitsdc  12444  bitsp1  12448  divgcdnn  12482  algfx  12560  eucalgcvga  12566  lcmcllem  12575  lcmneg  12582  isprm6  12655  cncongrprm  12665  phimullem  12733  pcid  12833  pcgcd  12838  pcz  12841  4sqlem9  12895  4sqlem15  12914  4sqlem16  12915  imasex  13324  grpidd  13402  gsumress  13414  ismndd  13456  subsubm  13502  grpinvid1  13571  grpinvid2  13572  grplcan  13581  grpinvinv  13586  grpinvval2  13602  mulgass  13682  mulgpropdg  13687  subginv  13704  subgmulg  13711  issubg2m  13712  issubg4m  13716  subsubg  13720  eqger  13747  qusinv  13759  resghm  13783  conjsubgen  13801  rngrz  13895  isrngd  13902  ringidss  13978  isringd  13990  ringlz  13992  ringrz  13993  unitgrp  14065  0unit  14078  unitnegcl  14079  dvrass  14088  dvreq1  14091  dvrdir  14092  ringinvdv  14094  invrpropdg  14098  rhmunitinv  14127  issubrng2  14159  subsubrng  14163  subrg1  14180  issubrg2  14190  subsubrg  14194  lmod0vs  14270  lmodvs0  14271  lmodvneg1  14279  islss3  14328  lspsnsubg  14345  lspid  14346  lspssv  14347  lspidm  14350  lspsnneg  14369  sraval  14386  qus1  14475  zringmulg  14547  mulgrhm  14558  znidom  14606  tgcl  14723  tgclb  14724  tgss2  14738  ntrss3  14782  ntridm  14785  opnssneib  14815  ssnei2  14816  innei  14822  resttopon  14830  cnpnei  14878  cnntri  14883  lmss  14905  txcnp  14930  blpnfctr  15098  mopni2  15142  bdmopn  15163  climcncf  15243  ivthdec  15303  cnplimcim  15326  dvconst  15353  dvconstre  15355  dvef  15386  plymullem  15409  plycoeid3  15416  rpcxpneg  15566  abscxp  15574  sgmmul  15655  lgscllem  15671  lgsvalmod  15683  lgsdir2  15697  lgsquadlem2  15742  lgsquad2lem2  15746  upgredg  15927  usgruspgrben  15969  usgredg3  15997  cvgcmp2nlemabs  16331  trilpolemisumle  16337  trilpolemeq1  16339  trilpolemlt1  16340  nconstwlpolemgt0  16363  neapmkvlem  16366