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

Theorem 3ad2antl1 1177
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 753 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1153 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 1074
This theorem is referenced by:  simpl1  1204  simpl1l  1255  simpl1r  1257  smorndom  7585  omeulem1  7782  dif1en  8309  ordiso2  8536  infpssrlem4  9241  fin1a2lem9  9343  gchpwdom  9605  tskwun  9719  gruxp  9742  infregelb  11120  fzo1fzo0n0  12634  fsuppmapnn0fiub  12905  fsuppmapnn0fiubOLD  12906  fprodle  14847  muldvds2  15130  dvds2add  15138  dvds2sub  15139  dvdstr  15141  lcmfledvds  15468  mulgnnsubcl  17675  mulgpropd  17706  gexdvdsi  18119  ringidss  18698  reslmhm2  19176  issubassa  19447  obs2ss  20196  lsslindf  20292  mndvcl  20320  mhmvlin  20326  madurid  20573  restntr  21109  cnpnei  21191  upxp  21549  qtopss  21641  opnfbas  21768  fbasrn  21810  trfg  21817  ufilmax  21833  ustuqtop1  22167  prdsxmetlem  22295  nmoix  22655  nmoi2  22656  iimulcl  22858  mbfimaopn2  23544  lgsval4lem  25153  f1otrg  25871  brbtwn2  25905  colinearalg  25910  axsegconlem1  25917  0vtxrusgr  26604  clwwisshclwws  27059  clwwlkfo  27100  numclwlk1lem2fo  27438  lnosub  27844  pjspansn  28666  eulerpartlemb  30660  cnpconn  31440  mclspps  31709  nodenselem8  32068  curf  33619  mblfinlem2  33679  mblfinlem3  33680  mettrifi  33785  ghomdiv  33923  grpokerinj  33924  rngohomco  34005  crngohomfo  34037  keridl  34063  cvrcon3b  34984  mzpsubst  37730  lzunuz  37750  diophrex  37758  rmxycomplete  37901  jm2.26  37988  lnmepi  38074  lmhmlnmsplit  38076  ntrclsiso  38784  ntrclskb  38786  ntrclsk3  38787  uzwo4  39637  wessf1ornlem  39787  choicefi  39808  supxrgere  39964  supxrgelem  39968  supxrge  39969  suplesup  39970  infxr  39998  infleinflem2  40002  rexabslelem  40060  fmul01lt1  40238  limcleqr  40296  limclner  40303  dvnprodlem1  40581  volioc  40608  stoweidlem60  40697  wallispilem3  40704  fourierdlem12  40756  fourierdlem41  40785  fourierdlem42  40786  fourierdlem48  40791  fourierdlem49  40792  fourierdlem54  40797  fourierdlem68  40811  fourierdlem73  40816  fourierdlem74  40817  fourierdlem75  40818  fourierdlem83  40826  elaa2  40871  etransclem24  40895  etransclem32  40903  ioorrnopnlem  40944  issalnnd  40983  sge0xaddlem2  41071  sge0seq  41083  meaiininc2  41125  hoicvr  41185  ovnsubaddlem2  41208  hoidmvval0  41224  hoidmvlelem3  41234  hspmbllem2  41264  vonioo  41319  vonicc  41322  smfinflem  41446  fmtnoprmfac2lem1  41905  fmtnofac1  41909  lincresunit3lem3  42690  suppdm  42727
  Copyright terms: Public domain W3C validator