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

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

Proof of Theorem 3ad2antl1
StepHypRef Expression
1 3ad2antl.1 . . 3 ((𝜑𝜒) → 𝜃)
21adantlr 746 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1210 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:  smorndom  7329  omeulem1  7526  dif1en  8055  ordiso2  8280  infpssrlem4  8988  fin1a2lem9  9090  gchpwdom  9348  tskwun  9462  gruxp  9485  infregelb  10856  fzo1fzo0n0  12343  fsuppmapnn0fiub  12609  fsuppmapnn0fiubOLD  12610  fprodle  14514  muldvds2  14793  dvds2add  14801  dvds2sub  14802  dvdstr  14804  lcmfledvds  15131  mulgnnsubcl  17324  mulgpropd  17355  gexdvdsi  17769  ringidss  18348  reslmhm2  18822  issubassa  19093  obs2ss  19839  lsslindf  19935  mndvcl  19963  mhmvlin  19969  madurid  20216  restntr  20743  cnpnei  20825  upxp  21183  qtopss  21275  opnfbas  21403  fbasrn  21445  trfg  21452  ufilmax  21468  ustuqtop1  21802  prdsxmetlem  21930  nmoix  22290  nmoi2  22291  iimulcl  22491  mbfimaopn2  23174  lgsval4lem  24777  f1otrg  25496  brbtwn2  25530  colinearalg  25535  axsegconlem1  25542  redwlk  25929  vdn1frgrav2  26345  usg2spot2nb  26385  numclwlk1lem2fo  26415  lnosub  26791  pjspansn  27613  eulerpartlemb  29550  cnpcon  30259  mclspps  30528  nodenselem8  30880  curf  32340  mblfinlem2  32400  mblfinlem3  32401  mettrifi  32506  ghomdiv  32644  grpokerinj  32645  rngohomco  32726  crngohomfo  32758  keridl  32784  cvrcon3b  33365  mzpsubst  36112  lzunuz  36132  diophrex  36140  rmxycomplete  36283  jm2.26  36370  lnmepi  36456  lmhmlnmsplit  36458  ntrclsiso  37168  ntrclskb  37170  ntrclsk3  37171  uzwo4  38029  wessf1ornlem  38149  choicefi  38170  supxrgere  38273  supxrgelem  38277  supxrge  38278  suplesup  38279  infxr  38307  infleinflem2  38311  fmul01lt1  38436  limcleqr  38494  limclner  38501  dvnprodlem1  38619  volioc  38647  stoweidlem60  38736  wallispilem3  38743  fourierdlem12  38795  fourierdlem41  38824  fourierdlem42  38825  fourierdlem48  38830  fourierdlem49  38831  fourierdlem54  38836  fourierdlem68  38850  fourierdlem73  38855  fourierdlem74  38856  fourierdlem75  38857  fourierdlem83  38865  elaa2  38910  etransclem24  38934  etransclem32  38942  ioorrnopnlem  38983  issalnnd  39022  sge0xaddlem2  39110  sge0seq  39122  meaiininc2  39161  hoicvr  39221  ovnsubaddlem2  39244  hoidmvval0  39260  hoidmvlelem3  39270  hspmbllem2  39300  vonioo  39356  vonicc  39359  fmtnoprmfac2lem1  39800  fmtnofac1  39804  0vtxrusgr  40758  clwwlksfo  41206  clwwisshclwws  41216  av-extwwlkfablem2  41491  av-numclwlk1lem2fo  41506  lincresunit3lem3  42038  suppdm  42075
  Copyright terms: Public domain W3C validator