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

Theorem 3ad2antl3 1203
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 752 . 2 (((𝜏𝜑) ∧ 𝜒) → 𝜃)
323adantl1 1172 1 (((𝜓𝜏𝜑) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  simpl3  1232  simpl3l  1287  simpl3r  1289  simpl31  1327  simpl32  1329  simpl33  1331  rspc3ev  3465  brcogw  5446  cocan1  6709  ov6g  6963  dif1en  8358  cfsmolem  9284  coftr  9287  axcc3  9452  axdc4lem  9469  gruf  9825  dedekindle  10393  zdivmul  11641  cshimadifsn  13775  fprodle  14926  bpolycl  14982  lcmdvds  15523  coprmdvdsOLD  15569  lubss  17322  gsumccat  17579  odeq  18169  ghmplusg  18449  lmhmvsca  19247  islindf4  20379  mndifsplit  20644  gsummatr01lem3  20665  gsummatr01  20667  mp2pm2mplem4  20816  elcls  21079  cnpresti  21294  cmpsublem  21404  comppfsc  21537  ptpjcn  21616  elfm3  21955  rnelfmlem  21957  nmoix  22734  caublcls  23307  ig1pdvds  24135  coeid3  24195  amgm  24916  brbtwn2  25984  colinearalg  25989  axsegconlem1  25996  ax5seglem1  26007  ax5seglem2  26008  edginwlkOLD  26741  homco1  28969  hoadddi  28971  br6  31954  lindsenlbs  33717  upixp  33837  filbcmb  33848  3dim1  35256  llni  35297  lplni  35321  lvoli  35364  cdleme42mgN  36278  mzprename  37814  infmrgelbi  37944  relexpxpmin  38511  n0p  39708  rexabslelem  40143  limcleqr  40379  fnlimfvre  40409  stoweidlem17  40737  stoweidlem28  40748  fourierdlem12  40839  fourierdlem41  40868  fourierdlem42  40869  fourierdlem74  40900  fourierdlem77  40903  qndenserrnopnlem  41020  issalnnd  41066  hspmbllem2  41347  issmfle  41460  smflimlem2  41486  smflimmpt  41522  smfinflem  41529  smflimsuplem7  41538  smflimsupmpt  41541  smfliminfmpt  41544  lighneallem3  42034
  Copyright terms: Public domain W3C validator