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

Theorem 3ad2antl3 1223
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 749 . 2 (((𝜏𝜑) ∧ 𝜒) → 𝜃)
323adantl1 1215 1 (((𝜓𝜏𝜑) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  rspc3ev  3321  brcogw  5279  cocan1  6531  ov6g  6783  dif1en  8178  cfsmolem  9077  coftr  9080  axcc3  9245  axdc4lem  9262  gruf  9618  dedekindle  10186  zdivmul  11434  cshimadifsn  13556  fprodle  14708  bpolycl  14764  lcmdvds  15302  coprmdvdsOLD  15348  lubss  17102  gsumccat  17359  odeq  17950  ghmplusg  18230  lmhmvsca  19026  islindf4  20158  mndifsplit  20423  gsummatr01lem3  20444  gsummatr01  20446  mp2pm2mplem4  20595  elcls  20858  cnpresti  21073  cmpsublem  21183  comppfsc  21316  ptpjcn  21395  elfm3  21735  rnelfmlem  21737  nmoix  22514  caublcls  23088  ig1pdvds  23917  coeid3  23977  amgm  24698  brbtwn2  25766  colinearalg  25771  axsegconlem1  25778  ax5seglem1  25789  ax5seglem2  25790  edginwlkOLD  26512  homco1  28630  hoadddi  28632  br6  31622  lindsenlbs  33375  upixp  33495  filbcmb  33506  3dim1  34572  llni  34613  lplni  34637  lvoli  34680  cdleme42mgN  35595  mzprename  37131  infmrgelbi  37261  relexpxpmin  37828  n0p  39029  rexabslelem  39458  limcleqr  39676  fnlimfvre  39706  stoweidlem17  39997  stoweidlem28  40008  fourierdlem12  40099  fourierdlem41  40128  fourierdlem42  40129  fourierdlem74  40160  fourierdlem77  40163  qndenserrnopnlem  40280  issalnnd  40326  hspmbllem2  40604  issmfle  40717  smflimlem2  40743  smflimmpt  40779  smfinflem  40786  smflimsuplem7  40795  smflimsupmpt  40798  smfliminfmpt  40801  lighneallem3  41289
  Copyright terms: Public domain W3C validator