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  3079  csbied2  3185  elpw2g  4267  pofun  4432  tfi  4703  fnbr  5459  caovlem2d  6246  caofcom  6296  fnexALT  6303  tfr1onlemres  6579  tfrcllemres  6592  tfri3  6597  ixpexgg  6956  f1domg  6996  fundmfi  7203  f1ofi  7209  finacn  7510  archnqq  7731  nqpru  7866  ltaddpr  7911  1idsr  8082  addgt0sr  8089  suplocsrlempr  8121  gt0ap0  8899  ap0gt0  8913  mulgt1  9136  gt0div  9143  ge0div  9144  ltdiv2  9160  creur  9232  avgle1  9478  recnz  9670  qreccl  9973  xrrege0  10157  peano2fzor  10576  flqltnz  10646  flqdiv  10682  zmodcl  10705  frecuzrdgtcl  10773  frecuzrdgfunlem  10780  seqfveqg  10839  seq3fveq  10840  ser3mono  10848  seqsplitg  10850  seqcaopr2g  10855  iseqf1olemkle  10858  seq3f1olemqsumkj  10872  seq3f1olemqsumk  10873  seqf1oglem2  10881  seqf1og  10882  seq3id  10886  seq3z  10889  seqhomog  10891  le2sq2  10976  bcpasc  11127  fihasheqf1oi  11148  seq3coll  11210  wrdnval  11251  wrdsymb1  11257  lswcl  11271  ccatlid  11290  ccatass  11292  ccat1st1st  11325  lswccats1fst  11328  swrdlsw  11357  ccatswrd  11358  pfxtrcfvl  11385  pfxsuff1eqwrdeq  11387  ccatpfx  11389  pfx1  11391  pfxswrd  11394  pfxlswccat  11401  swrdccatin2  11417  pfxccatin12  11421  caucvgrelemcau  11661  caucvgre  11662  r19.2uz  11674  sqrtgt0  11715  xrmaxiflemval  11931  clim2ser  12018  clim2ser2  12019  climub  12025  serf0  12033  fsumf1o  12072  fisumss  12074  fsumcl2lem  12080  fsumsplit  12089  fsum2dlemstep  12116  fisumrev2  12128  fsumlessfi  12142  telfsumo  12148  fsumparts  12152  fsumiun  12159  binom1dif  12169  isumsplit  12173  isumrpcl  12176  isumlessdc  12178  explecnv  12187  cvgratnnlemmn  12207  cvgratz  12214  cvgratgt0  12215  mertenslemi1  12217  clim2prod  12221  clim2divap  12222  fprodseq  12265  fprodf1o  12270  prodssdc  12271  fprodssdc  12272  fprodsplitdc  12278  fprodeq0  12299  fprod2dlemstep  12304  ef0lem  12342  eftlub  12372  tanval3ap  12396  dvdssubr  12521  divalgmod  12609  bitsdc  12629  bitsp1  12633  divgcdnn  12667  algfx  12745  eucalgcvga  12751  lcmcllem  12760  lcmneg  12767  isprm6  12840  cncongrprm  12850  phimullem  12918  pcid  13018  pcgcd  13023  pcz  13026  4sqlem9  13080  4sqlem15  13099  4sqlem16  13100  imasex  13510  grpidd  13588  gsumress  13600  ismndd  13642  subsubm  13688  grpinvid1  13757  grpinvid2  13758  grplcan  13767  grpinvinv  13772  grpinvval2  13788  mulgass  13868  mulgpropdg  13873  subginv  13890  subgmulg  13897  issubg2m  13898  issubg4m  13902  subsubg  13906  eqger  13933  qusinv  13945  resghm  13969  conjsubgen  13987  rngrz  14082  isrngd  14089  ringidss  14165  isringd  14177  ringlz  14179  ringrz  14180  unitgrp  14253  0unit  14266  unitnegcl  14267  dvrass  14276  dvreq1  14279  dvrdir  14280  ringinvdv  14282  invrpropdg  14286  rhmunitinv  14315  issubrng2  14347  subsubrng  14351  subrg1  14368  issubrg2  14378  subsubrg  14382  lmod0vs  14461  lmodvs0  14462  lmodvneg1  14470  islss3  14519  lspsnsubg  14536  lspid  14537  lspssv  14538  lspidm  14541  lspsnneg  14560  sraval  14577  qus1  14666  zringmulg  14738  mulgrhm  14749  znidom  14797  tgcl  14921  tgclb  14922  tgss2  14936  ntrss3  14980  ntridm  14983  opnssneib  15013  ssnei2  15014  innei  15020  resttopon  15028  cnpnei  15076  cnntri  15081  lmss  15103  txcnp  15128  blpnfctr  15296  mopni2  15340  bdmopn  15361  climcncf  15441  ivthdec  15501  cnplimcim  15524  dvconst  15551  dvconstre  15553  dvef  15584  plymullem  15607  plycoeid3  15614  rpcxpneg  15764  abscxp  15772  sgmmul  15856  lgscllem  15872  lgsvalmod  15884  lgsdir2  15898  lgsquadlem2  15943  lgsquad2lem2  15947  upgredg  16131  usgruspgrben  16173  usgredg3  16201  cvgcmp2nlemabs  16808  trilpolemisumle  16814  trilpolemeq1  16816  trilpolemlt1  16817  nconstwlpolemgt0  16841  neapmkvlem  16844