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

Theorem 3ad2antl1 1229
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 697 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1201 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:  simpl1  1235  simpl1l  1286  simpl1r  1288  simpl11  1322  simpl12  1324  simpl13  1326  smorndom  7711  omeulem1  7909  dif1en  8442  ordiso2  8669  infpssrlem4  9423  fin1a2lem9  9525  gchpwdom  9787  tskwun  9901  gruxp  9924  infregelb  11302  fzo1fzo0n0  12763  fsuppmapnn0fiub  13034  fprodle  14967  muldvds2  15250  dvds2add  15258  dvds2sub  15259  dvdstr  15261  lcmfledvds  15584  mulgnnsubcl  17778  mulgpropd  17806  gexdvdsi  18219  ringidss  18799  reslmhm2  19280  issubassa  19553  obs2ss  20304  lsslindf  20400  mndvcl  20428  mhmvlin  20434  madurid  20682  restntr  21221  cnpnei  21303  upxp  21661  qtopss  21753  opnfbas  21880  fbasrn  21922  trfg  21929  ufilmax  21945  ustuqtop1  22279  prdsxmetlem  22407  nmoix  22767  nmoi2  22768  iimulcl  22970  mbfimaopn2  23661  lgsval4lem  25270  f1otrg  25988  brbtwn2  26022  colinearalg  26027  axsegconlem1  26034  0vtxrusgr  26724  clwwisshclwws  27181  clwwlkfo  27222  numclwwlk1lem2fo  27560  lnosub  27965  pjspansn  28787  eulerpartlemb  30778  cnpconn  31557  mclspps  31826  nodenselem8  32184  curf  33719  mblfinlem2  33779  mblfinlem3  33780  mettrifi  33883  ghomdiv  34021  grpokerinj  34022  rngohomco  34103  crngohomfo  34135  keridl  34161  cvrcon3b  35076  mzpsubst  37831  lzunuz  37851  diophrex  37859  rmxycomplete  38001  jm2.26  38088  lnmepi  38174  lmhmlnmsplit  38176  ntrclsiso  38883  ntrclskb  38885  ntrclsk3  38886  uzwo4  39732  wessf1ornlem  39878  choicefi  39897  supxrgere  40047  supxrgelem  40051  supxrge  40052  suplesup  40053  infxr  40081  infleinflem2  40085  rexabslelem  40142  fmul01lt1  40316  limcleqr  40374  limclner  40381  dvnprodlem1  40659  volioc  40685  stoweidlem60  40774  wallispilem3  40781  fourierdlem12  40833  fourierdlem41  40862  fourierdlem42  40863  fourierdlem48  40868  fourierdlem49  40869  fourierdlem54  40874  fourierdlem68  40888  fourierdlem73  40893  fourierdlem74  40894  fourierdlem75  40895  fourierdlem83  40903  elaa2  40948  etransclem24  40972  etransclem32  40980  ioorrnopnlem  41021  issalnnd  41060  sge0xaddlem2  41148  sge0seq  41160  meaiininc2  41202  hoicvr  41262  ovnsubaddlem2  41285  hoidmvval0  41301  hoidmvlelem3  41311  hspmbllem2  41341  vonioo  41396  vonicc  41399  smfinflem  41523  fmtnoprmfac2lem1  42071  fmtnofac1  42075  lincresunit3lem3  42849  suppdm  42886
  Copyright terms: Public domain W3C validator