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  3082  csbied2  3188  elpw2g  4270  pofun  4435  tfi  4706  fnbr  5462  caovlem2d  6249  caofcom  6299  fnexALT  6306  tfr1onlemres  6582  tfrcllemres  6595  tfri3  6600  ixpexgg  6959  f1domg  6999  fundmfi  7206  f1ofi  7212  finacn  7513  archnqq  7734  nqpru  7869  ltaddpr  7914  1idsr  8085  addgt0sr  8092  suplocsrlempr  8124  gt0ap0  8902  ap0gt0  8916  mulgt1  9139  gt0div  9146  ge0div  9147  ltdiv2  9163  creur  9235  avgle1  9481  recnz  9674  qreccl  9977  xrrege0  10161  peano2fzor  10581  flqltnz  10651  flqdiv  10687  zmodcl  10710  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  seqfveqg  10844  seq3fveq  10845  ser3mono  10853  seqsplitg  10855  seqcaopr2g  10860  iseqf1olemkle  10863  seq3f1olemqsumkj  10877  seq3f1olemqsumk  10878  seqf1oglem2  10886  seqf1og  10887  seq3id  10891  seq3z  10894  seqhomog  10896  le2sq2  10981  bcpasc  11132  fihasheqf1oi  11154  seq3coll  11218  wrdnval  11259  wrdsymb1  11265  lswcl  11279  ccatlid  11298  ccatass  11300  ccat1st1st  11333  lswccats1fst  11336  swrdlsw  11365  ccatswrd  11366  pfxtrcfvl  11393  pfxsuff1eqwrdeq  11395  ccatpfx  11397  pfx1  11399  pfxswrd  11402  pfxlswccat  11409  swrdccatin2  11425  pfxccatin12  11429  caucvgrelemcau  11669  caucvgre  11670  r19.2uz  11682  sqrtgt0  11723  xrmaxiflemval  11939  clim2ser  12026  clim2ser2  12027  climub  12033  serf0  12041  fsumf1o  12080  fisumss  12082  fsumcl2lem  12088  fsumsplit  12097  fsum2dlemstep  12124  fisumrev2  12136  fsumlessfi  12150  telfsumo  12156  fsumparts  12160  fsumiun  12167  binom1dif  12177  isumsplit  12181  isumrpcl  12184  isumlessdc  12186  explecnv  12195  cvgratnnlemmn  12215  cvgratz  12222  cvgratgt0  12223  mertenslemi1  12225  clim2prod  12229  clim2divap  12230  fprodseq  12273  fprodf1o  12278  prodssdc  12279  fprodssdc  12280  fprodsplitdc  12286  fprodeq0  12307  fprod2dlemstep  12312  ef0lem  12350  eftlub  12380  tanval3ap  12404  dvdssubr  12529  divalgmod  12617  bitsdc  12637  bitsp1  12641  divgcdnn  12675  algfx  12753  eucalgcvga  12759  lcmcllem  12768  lcmneg  12775  isprm6  12848  cncongrprm  12858  phimullem  12926  pcid  13026  pcgcd  13031  pcz  13034  4sqlem9  13088  4sqlem15  13107  4sqlem16  13108  ballotfilemfc0  13153  ballotfilemfcc  13154  imasex  13535  grpidd  13613  gsumress  13625  ismndd  13667  subsubm  13713  grpinvid1  13782  grpinvid2  13783  grplcan  13792  grpinvinv  13797  grpinvval2  13813  mulgass  13893  mulgpropdg  13898  subginv  13915  subgmulg  13922  issubg2m  13923  issubg4m  13927  subsubg  13931  eqger  13958  qusinv  13970  resghm  13994  conjsubgen  14012  rngrz  14107  isrngd  14114  ringidss  14190  isringd  14202  ringlz  14204  ringrz  14205  unitgrp  14278  0unit  14291  unitnegcl  14292  dvrass  14301  dvreq1  14304  dvrdir  14305  ringinvdv  14307  invrpropdg  14311  rhmunitinv  14340  issubrng2  14372  subsubrng  14376  subrg1  14393  issubrg2  14403  subsubrg  14407  lmod0vs  14486  lmodvs0  14487  lmodvneg1  14495  islss3  14544  lspsnsubg  14561  lspid  14562  lspssv  14563  lspidm  14566  lspsnneg  14585  sraval  14602  qus1  14691  zringmulg  14763  mulgrhm  14774  znidom  14822  tgcl  14946  tgclb  14947  tgss2  14961  ntrss3  15005  ntridm  15008  opnssneib  15038  ssnei2  15039  innei  15045  resttopon  15053  cnpnei  15101  cnntri  15106  lmss  15128  txcnp  15153  blpnfctr  15321  mopni2  15365  bdmopn  15386  climcncf  15466  ivthdec  15526  cnplimcim  15549  dvconst  15576  dvconstre  15578  dvef  15609  plymullem  15632  plycoeid3  15639  rpcxpneg  15789  abscxp  15797  sgmmul  15881  lgscllem  15897  lgsvalmod  15909  lgsdir2  15923  lgsquadlem2  15968  lgsquad2lem2  15972  upgredg  16156  usgruspgrben  16198  usgredg3  16226  cvgcmp2nlemabs  16833  trilpolemisumle  16839  trilpolemeq1  16841  trilpolemlt1  16842  nconstwlpolemgt0  16867  neapmkvlem  16870