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  3024  csbied2  3129  elpw2g  4186  pofun  4344  tfi  4615  fnbr  5357  caovlem2d  6113  caofcom  6158  fnexALT  6165  tfr1onlemres  6404  tfrcllemres  6417  tfri3  6422  ixpexgg  6778  f1domg  6814  fundmfi  6998  f1ofi  7004  archnqq  7479  nqpru  7614  ltaddpr  7659  1idsr  7830  addgt0sr  7837  suplocsrlempr  7869  gt0ap0  8647  ap0gt0  8661  mulgt1  8884  gt0div  8891  ge0div  8892  ltdiv2  8908  creur  8980  avgle1  9226  recnz  9413  qreccl  9710  xrrege0  9894  peano2fzor  10302  flqltnz  10359  flqdiv  10395  zmodcl  10418  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  seqfveqg  10552  seq3fveq  10553  ser3mono  10561  seqsplitg  10563  seqcaopr2g  10568  iseqf1olemkle  10571  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seqf1oglem2  10594  seqf1og  10595  seq3id  10599  seq3z  10602  seqhomog  10604  le2sq2  10689  bcpasc  10840  fihasheqf1oi  10861  seq3coll  10916  wrdnval  10947  wrdsymb1  10953  caucvgrelemcau  11127  caucvgre  11128  r19.2uz  11140  sqrtgt0  11181  xrmaxiflemval  11396  clim2ser  11483  clim2ser2  11484  climub  11490  serf0  11498  fsumf1o  11536  fisumss  11538  fsumcl2lem  11544  fsumsplit  11553  fsum2dlemstep  11580  fisumrev2  11592  fsumlessfi  11606  telfsumo  11612  fsumparts  11616  fsumiun  11623  binom1dif  11633  isumsplit  11637  isumrpcl  11640  isumlessdc  11642  explecnv  11651  cvgratnnlemmn  11671  cvgratz  11678  cvgratgt0  11679  mertenslemi1  11681  clim2prod  11685  clim2divap  11686  fprodseq  11729  fprodf1o  11734  prodssdc  11735  fprodssdc  11736  fprodsplitdc  11742  fprodeq0  11763  fprod2dlemstep  11768  ef0lem  11806  eftlub  11836  tanval3ap  11860  dvdssubr  11985  divalgmod  12071  divgcdnn  12115  algfx  12193  eucalgcvga  12199  lcmcllem  12208  lcmneg  12215  isprm6  12288  cncongrprm  12298  phimullem  12366  pcid  12465  pcgcd  12470  pcz  12473  4sqlem9  12527  4sqlem15  12546  4sqlem16  12547  imasex  12891  grpidd  12969  gsumress  12981  ismndd  13021  subsubm  13058  grpinvid1  13127  grpinvid2  13128  grplcan  13137  grpinvinv  13142  grpinvval2  13158  mulgass  13232  mulgpropdg  13237  subginv  13254  subgmulg  13261  issubg2m  13262  issubg4m  13266  subsubg  13270  eqger  13297  qusinv  13309  resghm  13333  conjsubgen  13351  rngrz  13445  isrngd  13452  ringidss  13528  isringd  13540  ringlz  13542  ringrz  13543  unitgrp  13615  0unit  13628  unitnegcl  13629  dvrass  13638  dvreq1  13641  dvrdir  13642  ringinvdv  13644  invrpropdg  13648  rhmunitinv  13677  issubrng2  13709  subsubrng  13713  subrg1  13730  issubrg2  13740  subsubrg  13744  lmod0vs  13820  lmodvs0  13821  lmodvneg1  13829  islss3  13878  lspsnsubg  13895  lspid  13896  lspssv  13897  lspidm  13900  lspsnneg  13919  sraval  13936  qus1  14025  zringmulg  14097  mulgrhm  14108  znidom  14156  tgcl  14243  tgclb  14244  tgss2  14258  ntrss3  14302  ntridm  14305  opnssneib  14335  ssnei2  14336  innei  14342  resttopon  14350  cnpnei  14398  cnntri  14403  lmss  14425  txcnp  14450  blpnfctr  14618  mopni2  14662  bdmopn  14683  climcncf  14763  ivthdec  14823  cnplimcim  14846  dvconst  14873  dvconstre  14875  dvef  14906  plymullem  14929  rpcxpneg  15083  abscxp  15090  lgscllem  15164  lgsvalmod  15176  lgsdir2  15190  lgsquadlem2  15235  lgsquad2lem2  15239  cvgcmp2nlemabs  15592  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  nconstwlpolemgt0  15624  neapmkvlem  15627