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  3067  csbied2  3173  elpw2g  4244  pofun  4407  tfi  4678  fnbr  5431  caovlem2d  6210  caofcom  6261  fnexALT  6268  tfr1onlemres  6510  tfrcllemres  6523  tfri3  6528  ixpexgg  6886  f1domg  6926  fundmfi  7130  f1ofi  7136  finacn  7412  archnqq  7630  nqpru  7765  ltaddpr  7810  1idsr  7981  addgt0sr  7988  suplocsrlempr  8020  gt0ap0  8799  ap0gt0  8813  mulgt1  9036  gt0div  9043  ge0div  9044  ltdiv2  9060  creur  9132  avgle1  9378  recnz  9566  qreccl  9869  xrrege0  10053  peano2fzor  10470  flqltnz  10540  flqdiv  10576  zmodcl  10599  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  seqfveqg  10733  seq3fveq  10734  ser3mono  10742  seqsplitg  10744  seqcaopr2g  10749  iseqf1olemkle  10752  seq3f1olemqsumkj  10766  seq3f1olemqsumk  10767  seqf1oglem2  10775  seqf1og  10776  seq3id  10780  seq3z  10783  seqhomog  10785  le2sq2  10870  bcpasc  11021  fihasheqf1oi  11042  seq3coll  11099  wrdnval  11137  wrdsymb1  11143  lswcl  11157  ccatlid  11176  ccatass  11178  ccat1st1st  11211  lswccats1fst  11214  swrdlsw  11243  ccatswrd  11244  pfxtrcfvl  11271  pfxsuff1eqwrdeq  11273  ccatpfx  11275  pfx1  11277  pfxswrd  11280  pfxlswccat  11287  swrdccatin2  11303  pfxccatin12  11307  caucvgrelemcau  11534  caucvgre  11535  r19.2uz  11547  sqrtgt0  11588  xrmaxiflemval  11804  clim2ser  11891  clim2ser2  11892  climub  11898  serf0  11906  fsumf1o  11944  fisumss  11946  fsumcl2lem  11952  fsumsplit  11961  fsum2dlemstep  11988  fisumrev2  12000  fsumlessfi  12014  telfsumo  12020  fsumparts  12024  fsumiun  12031  binom1dif  12041  isumsplit  12045  isumrpcl  12048  isumlessdc  12050  explecnv  12059  cvgratnnlemmn  12079  cvgratz  12086  cvgratgt0  12087  mertenslemi1  12089  clim2prod  12093  clim2divap  12094  fprodseq  12137  fprodf1o  12142  prodssdc  12143  fprodssdc  12144  fprodsplitdc  12150  fprodeq0  12171  fprod2dlemstep  12176  ef0lem  12214  eftlub  12244  tanval3ap  12268  dvdssubr  12393  divalgmod  12481  bitsdc  12501  bitsp1  12505  divgcdnn  12539  algfx  12617  eucalgcvga  12623  lcmcllem  12632  lcmneg  12639  isprm6  12712  cncongrprm  12722  phimullem  12790  pcid  12890  pcgcd  12895  pcz  12898  4sqlem9  12952  4sqlem15  12971  4sqlem16  12972  imasex  13381  grpidd  13459  gsumress  13471  ismndd  13513  subsubm  13559  grpinvid1  13628  grpinvid2  13629  grplcan  13638  grpinvinv  13643  grpinvval2  13659  mulgass  13739  mulgpropdg  13744  subginv  13761  subgmulg  13768  issubg2m  13769  issubg4m  13773  subsubg  13777  eqger  13804  qusinv  13816  resghm  13840  conjsubgen  13858  rngrz  13952  isrngd  13959  ringidss  14035  isringd  14047  ringlz  14049  ringrz  14050  unitgrp  14123  0unit  14136  unitnegcl  14137  dvrass  14146  dvreq1  14149  dvrdir  14150  ringinvdv  14152  invrpropdg  14156  rhmunitinv  14185  issubrng2  14217  subsubrng  14221  subrg1  14238  issubrg2  14248  subsubrg  14252  lmod0vs  14328  lmodvs0  14329  lmodvneg1  14337  islss3  14386  lspsnsubg  14403  lspid  14404  lspssv  14405  lspidm  14408  lspsnneg  14427  sraval  14444  qus1  14533  zringmulg  14605  mulgrhm  14616  znidom  14664  tgcl  14781  tgclb  14782  tgss2  14796  ntrss3  14840  ntridm  14843  opnssneib  14873  ssnei2  14874  innei  14880  resttopon  14888  cnpnei  14936  cnntri  14941  lmss  14963  txcnp  14988  blpnfctr  15156  mopni2  15200  bdmopn  15221  climcncf  15301  ivthdec  15361  cnplimcim  15384  dvconst  15411  dvconstre  15413  dvef  15444  plymullem  15467  plycoeid3  15474  rpcxpneg  15624  abscxp  15632  sgmmul  15713  lgscllem  15729  lgsvalmod  15741  lgsdir2  15755  lgsquadlem2  15800  lgsquad2lem2  15804  upgredg  15988  usgruspgrben  16030  usgredg3  16058  cvgcmp2nlemabs  16586  trilpolemisumle  16592  trilpolemeq1  16594  trilpolemlt1  16595  nconstwlpolemgt0  16618  neapmkvlem  16621