MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ad2antl3 Structured version   Visualization version   GIF version

Theorem 3ad2antl3 1217
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
3ad2antl3 (((𝜓𝜏𝜑) ∧ 𝜒) → 𝜃)

Proof of Theorem 3ad2antl3
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantll 745 . 2 (((𝜏𝜑) ∧ 𝜒) → 𝜃)
323adantl1 1209 1 (((𝜓𝜏𝜑) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032
This theorem is referenced by:  rspc3ev  3291  brcogw  5195  cocan1  6419  ov6g  6669  dif1en  8050  cfsmolem  8947  coftr  8950  axcc3  9115  axdc4lem  9132  gruf  9484  dedekindle  10047  zdivmul  11276  cshimadifsn  13367  fprodle  14507  bpolycl  14563  lcmdvds  15100  coprmdvdsOLD  15146  lubss  16885  gsumccat  17142  odeq  17733  ghmplusg  18013  lmhmvsca  18807  islindf4  19933  mndifsplit  20198  gsummatr01lem3  20219  gsummatr01  20221  mp2pm2mplem4  20370  elcls  20624  cnpresti  20839  cmpsublem  20949  comppfsc  21082  ptpjcn  21161  elfm3  21501  rnelfmlem  21503  nmoix  22270  caublcls  22827  ig1pdvds  23652  coeid3  23712  amgm  24429  brbtwn2  25498  colinearalg  25503  axsegconlem1  25510  ax5seglem1  25521  ax5seglem2  25522  usgra2edg  25672  clwwlkel  26082  clwwisshclww  26096  homco1  27845  hoadddi  27847  br6  30701  lindsenlbs  32372  upixp  32492  filbcmb  32503  3dim1  33569  llni  33610  lplni  33634  lvoli  33677  cdleme42mgN  34592  mzprename  36128  infmrgelbi  36258  relexpxpmin  36826  n0p  38032  limcleqr  38510  fnlimfvre  38540  stoweidlem17  38709  stoweidlem28  38720  fourierdlem12  38811  fourierdlem41  38840  fourierdlem42  38841  fourierdlem74  38872  fourierdlem77  38875  qndenserrnopnlem  38992  issalnnd  39038  hspmbllem2  39316  issmfle  39431  smflimlem2  39457  lighneallem3  39862  edginwlk  40836
  Copyright terms: Public domain W3C validator