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

Theorem 3ad2antl3 1184
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 713 . 2 (((𝜏𝜑) ∧ 𝜒) → 𝜃)
323adantl1 1163 1 (((𝜓𝜏𝜑) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simpl3  1190  simpl3l  1225  simpl3r  1226  simpl31  1251  simpl32  1252  simpl33  1253  rspc3ev  3585  brcogw  5703  cocan1  7025  ov6g  7292  dif1en  8735  cfsmolem  9681  coftr  9684  axcc3  9849  axdc4lem  9866  gruf  10222  dedekindle  10793  zdivmul  12042  cshf1  14163  cshimadifsn  14182  fprodle  15342  bpolycl  15398  lcmdvds  15942  lubss  17723  gsumccatOLD  17997  odeq  18670  ghmplusg  18959  lmhmvsca  19810  islindf4  20527  mndifsplit  21241  gsummatr01lem3  21262  gsummatr01  21264  mp2pm2mplem4  21414  elcls  21678  cnpresti  21893  cmpsublem  22004  comppfsc  22137  ptpjcn  22216  elfm3  22555  rnelfmlem  22557  nmoix  23335  caublcls  23913  ig1pdvds  24777  coeid3  24837  amgm  25576  brbtwn2  26699  colinearalg  26704  axsegconlem1  26711  ax5seglem1  26722  ax5seglem2  26723  homco1  29584  hoadddi  29586  br6  33106  fpr1  33252  lindsenlbs  35052  upixp  35167  filbcmb  35178  3dim1  36763  llni  36804  lplni  36828  lvoli  36871  cdleme42mgN  37784  mzprename  39688  infmrgelbi  39817  relexpxpmin  40416  n0p  41675  rexabslelem  42053  limcleqr  42284  fnlimfvre  42314  stoweidlem17  42657  stoweidlem28  42668  fourierdlem12  42759  fourierdlem41  42788  fourierdlem42  42789  fourierdlem74  42820  fourierdlem77  42823  qndenserrnopnlem  42937  issalnnd  42983  hspmbllem2  43264  issmfle  43377  smflimlem2  43403  smflimmpt  43439  smfinflem  43446  smflimsuplem7  43455  smflimsupmpt  43458  smfliminfmpt  43461  lighneallem3  44123
  Copyright terms: Public domain W3C validator