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

Theorem 3ad2antl1 1243
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 751 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1238 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  smorndom  7510  omeulem1  7707  dif1en  8234  ordiso2  8461  infpssrlem4  9166  fin1a2lem9  9268  gchpwdom  9530  tskwun  9644  gruxp  9667  infregelb  11045  fzo1fzo0n0  12558  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  fprodle  14771  muldvds2  15054  dvds2add  15062  dvds2sub  15063  dvdstr  15065  lcmfledvds  15392  mulgnnsubcl  17600  mulgpropd  17631  gexdvdsi  18044  ringidss  18623  reslmhm2  19101  issubassa  19372  obs2ss  20121  lsslindf  20217  mndvcl  20245  mhmvlin  20251  madurid  20498  restntr  21034  cnpnei  21116  upxp  21474  qtopss  21566  opnfbas  21693  fbasrn  21735  trfg  21742  ufilmax  21758  ustuqtop1  22092  prdsxmetlem  22220  nmoix  22580  nmoi2  22581  iimulcl  22783  mbfimaopn2  23469  lgsval4lem  25078  f1otrg  25796  brbtwn2  25830  colinearalg  25835  axsegconlem1  25842  0vtxrusgr  26529  clwwisshclwws  26972  clwwlkfo  27013  numclwlk1lem2fo  27348  lnosub  27742  pjspansn  28564  eulerpartlemb  30558  cnpconn  31338  mclspps  31607  nodenselem8  31966  curf  33517  mblfinlem2  33577  mblfinlem3  33578  mettrifi  33683  ghomdiv  33821  grpokerinj  33822  rngohomco  33903  crngohomfo  33935  keridl  33961  cvrcon3b  34882  mzpsubst  37628  lzunuz  37648  diophrex  37656  rmxycomplete  37799  jm2.26  37886  lnmepi  37972  lmhmlnmsplit  37974  ntrclsiso  38682  ntrclskb  38684  ntrclsk3  38685  uzwo4  39535  wessf1ornlem  39685  choicefi  39706  supxrgere  39862  supxrgelem  39866  supxrge  39867  suplesup  39868  infxr  39896  infleinflem2  39900  rexabslelem  39958  fmul01lt1  40136  limcleqr  40194  limclner  40201  dvnprodlem1  40479  volioc  40506  stoweidlem60  40595  wallispilem3  40602  fourierdlem12  40654  fourierdlem41  40683  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem54  40695  fourierdlem68  40709  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem83  40724  elaa2  40769  etransclem24  40793  etransclem32  40801  ioorrnopnlem  40842  issalnnd  40881  sge0xaddlem2  40969  sge0seq  40981  meaiininc2  41023  hoicvr  41083  ovnsubaddlem2  41106  hoidmvval0  41122  hoidmvlelem3  41132  hspmbllem2  41162  vonioo  41217  vonicc  41220  smfinflem  41344  fmtnoprmfac2lem1  41803  fmtnofac1  41807  lincresunit3lem3  42588  suppdm  42625
  Copyright terms: Public domain W3C validator