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  962  stoic2a  1440  sbcied2  3027  csbied2  3132  elpw2g  4190  pofun  4348  tfi  4619  fnbr  5361  caovlem2d  6117  caofcom  6162  fnexALT  6169  tfr1onlemres  6408  tfrcllemres  6421  tfri3  6426  ixpexgg  6782  f1domg  6818  fundmfi  7004  f1ofi  7010  archnqq  7486  nqpru  7621  ltaddpr  7666  1idsr  7837  addgt0sr  7844  suplocsrlempr  7876  gt0ap0  8655  ap0gt0  8669  mulgt1  8892  gt0div  8899  ge0div  8900  ltdiv2  8916  creur  8988  avgle1  9234  recnz  9421  qreccl  9718  xrrege0  9902  peano2fzor  10310  flqltnz  10379  flqdiv  10415  zmodcl  10438  frecuzrdgtcl  10506  frecuzrdgfunlem  10513  seqfveqg  10572  seq3fveq  10573  ser3mono  10581  seqsplitg  10583  seqcaopr2g  10588  iseqf1olemkle  10591  seq3f1olemqsumkj  10605  seq3f1olemqsumk  10606  seqf1oglem2  10614  seqf1og  10615  seq3id  10619  seq3z  10622  seqhomog  10624  le2sq2  10709  bcpasc  10860  fihasheqf1oi  10881  seq3coll  10936  wrdnval  10967  wrdsymb1  10973  caucvgrelemcau  11147  caucvgre  11148  r19.2uz  11160  sqrtgt0  11201  xrmaxiflemval  11417  clim2ser  11504  clim2ser2  11505  climub  11511  serf0  11519  fsumf1o  11557  fisumss  11559  fsumcl2lem  11565  fsumsplit  11574  fsum2dlemstep  11601  fisumrev2  11613  fsumlessfi  11627  telfsumo  11633  fsumparts  11637  fsumiun  11644  binom1dif  11654  isumsplit  11658  isumrpcl  11661  isumlessdc  11663  explecnv  11672  cvgratnnlemmn  11692  cvgratz  11699  cvgratgt0  11700  mertenslemi1  11702  clim2prod  11706  clim2divap  11707  fprodseq  11750  fprodf1o  11755  prodssdc  11756  fprodssdc  11757  fprodsplitdc  11763  fprodeq0  11784  fprod2dlemstep  11789  ef0lem  11827  eftlub  11857  tanval3ap  11881  dvdssubr  12006  divalgmod  12094  bitsdc  12114  bitsp1  12118  divgcdnn  12152  algfx  12230  eucalgcvga  12236  lcmcllem  12245  lcmneg  12252  isprm6  12325  cncongrprm  12335  phimullem  12403  pcid  12503  pcgcd  12508  pcz  12511  4sqlem9  12565  4sqlem15  12584  4sqlem16  12585  imasex  12958  grpidd  13036  gsumress  13048  ismndd  13088  subsubm  13125  grpinvid1  13194  grpinvid2  13195  grplcan  13204  grpinvinv  13209  grpinvval2  13225  mulgass  13299  mulgpropdg  13304  subginv  13321  subgmulg  13328  issubg2m  13329  issubg4m  13333  subsubg  13337  eqger  13364  qusinv  13376  resghm  13400  conjsubgen  13418  rngrz  13512  isrngd  13519  ringidss  13595  isringd  13607  ringlz  13609  ringrz  13610  unitgrp  13682  0unit  13695  unitnegcl  13696  dvrass  13705  dvreq1  13708  dvrdir  13709  ringinvdv  13711  invrpropdg  13715  rhmunitinv  13744  issubrng2  13776  subsubrng  13780  subrg1  13797  issubrg2  13807  subsubrg  13811  lmod0vs  13887  lmodvs0  13888  lmodvneg1  13896  islss3  13945  lspsnsubg  13962  lspid  13963  lspssv  13964  lspidm  13967  lspsnneg  13986  sraval  14003  qus1  14092  zringmulg  14164  mulgrhm  14175  znidom  14223  tgcl  14310  tgclb  14311  tgss2  14325  ntrss3  14369  ntridm  14372  opnssneib  14402  ssnei2  14403  innei  14409  resttopon  14417  cnpnei  14465  cnntri  14470  lmss  14492  txcnp  14517  blpnfctr  14685  mopni2  14729  bdmopn  14750  climcncf  14830  ivthdec  14890  cnplimcim  14913  dvconst  14940  dvconstre  14942  dvef  14973  plymullem  14996  plycoeid3  15003  rpcxpneg  15153  abscxp  15161  sgmmul  15242  lgscllem  15258  lgsvalmod  15270  lgsdir2  15284  lgsquadlem2  15329  lgsquad2lem2  15333  cvgcmp2nlemabs  15686  trilpolemisumle  15692  trilpolemeq1  15694  trilpolemlt1  15695  nconstwlpolemgt0  15718  neapmkvlem  15721