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

Theorem 3ad2antl3 1231
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 696 . 2 (((𝜏𝜑) ∧ 𝜒) → 𝜃)
323adantl1 1200 1 (((𝜓𝜏𝜑) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simpl3  1239  simpl3l  1294  simpl3r  1296  simpl31  1334  simpl32  1336  simpl33  1338  rspc3ev  3530  brcogw  5506  cocan1  6780  ov6g  7038  dif1en  8442  cfsmolem  9387  coftr  9390  axcc3  9555  axdc4lem  9572  gruf  9928  dedekindle  10496  zdivmul  11735  cshimadifsn  13819  fprodle  14967  bpolycl  15023  lcmdvds  15560  lubss  17346  gsumccat  17603  odeq  18190  ghmplusg  18470  lmhmvsca  19272  islindf4  20408  mndifsplit  20674  gsummatr01lem3  20696  gsummatr01  20698  mp2pm2mplem4  20848  elcls  21112  cnpresti  21327  cmpsublem  21437  comppfsc  21570  ptpjcn  21649  elfm3  21988  rnelfmlem  21990  nmoix  22767  caublcls  23341  ig1pdvds  24173  coeid3  24233  amgm  24954  brbtwn2  26022  colinearalg  26027  axsegconlem1  26034  ax5seglem1  26045  ax5seglem2  26046  edginwlkOLD  26782  homco1  29011  hoadddi  29013  br6  31991  lindsenlbs  33736  upixp  33855  filbcmb  33866  3dim1  35266  llni  35307  lplni  35331  lvoli  35374  cdleme42mgN  36287  mzprename  37832  infmrgelbi  37962  relexpxpmin  38527  n0p  39720  rexabslelem  40142  limcleqr  40374  fnlimfvre  40404  stoweidlem17  40731  stoweidlem28  40742  fourierdlem12  40833  fourierdlem41  40862  fourierdlem42  40863  fourierdlem74  40894  fourierdlem77  40897  qndenserrnopnlem  41014  issalnnd  41060  hspmbllem2  41341  issmfle  41454  smflimlem2  41480  smflimmpt  41516  smfinflem  41523  smflimsuplem7  41532  smflimsupmpt  41535  smfliminfmpt  41538  lighneallem3  42117
  Copyright terms: Public domain W3C validator