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  963  stoic2a  1449  sbcied2  3038  csbied2  3143  elpw2g  4205  pofun  4364  tfi  4635  fnbr  5384  caovlem2d  6149  caofcom  6199  fnexALT  6206  tfr1onlemres  6445  tfrcllemres  6458  tfri3  6463  ixpexgg  6819  f1domg  6859  fundmfi  7051  f1ofi  7057  finacn  7329  archnqq  7543  nqpru  7678  ltaddpr  7723  1idsr  7894  addgt0sr  7901  suplocsrlempr  7933  gt0ap0  8712  ap0gt0  8726  mulgt1  8949  gt0div  8956  ge0div  8957  ltdiv2  8973  creur  9045  avgle1  9291  recnz  9479  qreccl  9776  xrrege0  9960  peano2fzor  10374  flqltnz  10443  flqdiv  10479  zmodcl  10502  frecuzrdgtcl  10570  frecuzrdgfunlem  10577  seqfveqg  10636  seq3fveq  10637  ser3mono  10645  seqsplitg  10647  seqcaopr2g  10652  iseqf1olemkle  10655  seq3f1olemqsumkj  10669  seq3f1olemqsumk  10670  seqf1oglem2  10678  seqf1og  10679  seq3id  10683  seq3z  10686  seqhomog  10688  le2sq2  10773  bcpasc  10924  fihasheqf1oi  10945  seq3coll  11000  wrdnval  11037  wrdsymb1  11043  lswcl  11057  ccatlid  11076  ccatass  11078  ccat1st1st  11107  lswccats1fst  11110  swrdlsw  11136  ccatswrd  11137  pfxtrcfvl  11162  pfxsuff1eqwrdeq  11164  ccatpfx  11166  pfx1  11168  pfxswrd  11171  caucvgrelemcau  11341  caucvgre  11342  r19.2uz  11354  sqrtgt0  11395  xrmaxiflemval  11611  clim2ser  11698  clim2ser2  11699  climub  11705  serf0  11713  fsumf1o  11751  fisumss  11753  fsumcl2lem  11759  fsumsplit  11768  fsum2dlemstep  11795  fisumrev2  11807  fsumlessfi  11821  telfsumo  11827  fsumparts  11831  fsumiun  11838  binom1dif  11848  isumsplit  11852  isumrpcl  11855  isumlessdc  11857  explecnv  11866  cvgratnnlemmn  11886  cvgratz  11893  cvgratgt0  11894  mertenslemi1  11896  clim2prod  11900  clim2divap  11901  fprodseq  11944  fprodf1o  11949  prodssdc  11950  fprodssdc  11951  fprodsplitdc  11957  fprodeq0  11978  fprod2dlemstep  11983  ef0lem  12021  eftlub  12051  tanval3ap  12075  dvdssubr  12200  divalgmod  12288  bitsdc  12308  bitsp1  12312  divgcdnn  12346  algfx  12424  eucalgcvga  12430  lcmcllem  12439  lcmneg  12446  isprm6  12519  cncongrprm  12529  phimullem  12597  pcid  12697  pcgcd  12702  pcz  12705  4sqlem9  12759  4sqlem15  12778  4sqlem16  12779  imasex  13187  grpidd  13265  gsumress  13277  ismndd  13319  subsubm  13365  grpinvid1  13434  grpinvid2  13435  grplcan  13444  grpinvinv  13449  grpinvval2  13465  mulgass  13545  mulgpropdg  13550  subginv  13567  subgmulg  13574  issubg2m  13575  issubg4m  13579  subsubg  13583  eqger  13610  qusinv  13622  resghm  13646  conjsubgen  13664  rngrz  13758  isrngd  13765  ringidss  13841  isringd  13853  ringlz  13855  ringrz  13856  unitgrp  13928  0unit  13941  unitnegcl  13942  dvrass  13951  dvreq1  13954  dvrdir  13955  ringinvdv  13957  invrpropdg  13961  rhmunitinv  13990  issubrng2  14022  subsubrng  14026  subrg1  14043  issubrg2  14053  subsubrg  14057  lmod0vs  14133  lmodvs0  14134  lmodvneg1  14142  islss3  14191  lspsnsubg  14208  lspid  14209  lspssv  14210  lspidm  14213  lspsnneg  14232  sraval  14249  qus1  14338  zringmulg  14410  mulgrhm  14421  znidom  14469  tgcl  14586  tgclb  14587  tgss2  14601  ntrss3  14645  ntridm  14648  opnssneib  14678  ssnei2  14679  innei  14685  resttopon  14693  cnpnei  14741  cnntri  14746  lmss  14768  txcnp  14793  blpnfctr  14961  mopni2  15005  bdmopn  15026  climcncf  15106  ivthdec  15166  cnplimcim  15189  dvconst  15216  dvconstre  15218  dvef  15249  plymullem  15272  plycoeid3  15279  rpcxpneg  15429  abscxp  15437  sgmmul  15518  lgscllem  15534  lgsvalmod  15546  lgsdir2  15560  lgsquadlem2  15605  lgsquad2lem2  15609  cvgcmp2nlemabs  16086  trilpolemisumle  16092  trilpolemeq1  16094  trilpolemlt1  16095  nconstwlpolemgt0  16118  neapmkvlem  16121