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

Theorem 3ad2antl1 1186
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 714 . 2 (((𝜑𝜏) ∧ 𝜒) → 𝜃)
323adantl2 1168 1 (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  simpl1  1192  simpl1l  1225  simpl1r  1226  simpl11  1249  simpl12  1250  simpl13  1251  smocdmdom  8315  omeulem1  8530  f1oen4g  8907  f1dom4g  8908  dif1ennnALT  9224  ordiso2  9456  infpssrlem4  10247  fin1a2lem9  10349  gchpwdom  10611  tskwun  10725  gruxp  10748  infregelb  12144  fzo1fzo0n0  13629  fsuppmapnn0fiub  13902  pfxsuffeqwrdeq  14592  fprodle  15884  muldvds2  16169  dvds2add  16177  dvds2sub  16178  dvdstr  16181  lcmfledvds  16513  mulgnnsubcl  18893  mulgpropd  18923  gexdvdsi  19370  ringidss  20003  reslmhm2  20529  obs2ss  21151  lsslindf  21252  issubassa  21288  mndvcl  21756  mhmvlin  21762  madurid  22009  restntr  22549  cnpnei  22631  upxp  22990  qtopss  23082  opnfbas  23209  fbasrn  23251  trfg  23258  ufilmax  23274  ustuqtop1  23609  prdsxmetlem  23737  nmoix  24109  nmoi2  24110  iimulcl  24316  mbfimaopn2  25037  lgsval4lem  26672  nodenselem8  27055  f1otrg  27855  brbtwn2  27896  colinearalg  27901  axsegconlem1  27908  0vtxrusgr  28567  clwwlkccatlem  28975  clwwlkccat  28976  clwwisshclwws  29001  clwwlkfo  29036  numclwwlk1lem2fo  29344  lnosub  29743  pjspansn  30561  eulerpartlemb  33025  cnpconn  33881  mclspps  34235  curf  36102  mblfinlem2  36162  mblfinlem3  36163  mettrifi  36262  ghomdiv  36397  grpokerinj  36398  rngohomco  36479  crngohomfo  36511  keridl  36537  cvrcon3b  37785  factwoffsmonot  40661  mzpsubst  41114  lzunuz  41134  diophrex  41141  rmxycomplete  41284  jm2.26  41369  lnmepi  41455  lmhmlnmsplit  41457  nadd2rabex  41745  nadd1rabtr  41747  nadd1rabex  41749  ntrclsiso  42427  ntrclskb  42429  ntrclsk3  42430  uzwo4  43349  wessf1ornlem  43491  choicefi  43508  supxrgere  43654  supxrgelem  43658  supxrge  43659  suplesup  43660  infxr  43688  infleinflem2  43692  rexabslelem  43739  fmul01lt1  43913  limcleqr  43971  limclner  43978  dvnprodlem1  44273  volioc  44299  stoweidlem60  44387  wallispilem3  44394  fourierdlem12  44446  fourierdlem41  44475  fourierdlem42  44476  fourierdlem48  44481  fourierdlem49  44482  fourierdlem54  44487  fourierdlem68  44501  fourierdlem73  44506  fourierdlem74  44507  fourierdlem75  44508  fourierdlem83  44516  elaa2  44561  etransclem24  44585  etransclem32  44593  ioorrnopnlem  44631  issalnnd  44672  sge0xaddlem2  44761  sge0seq  44773  meaiininc2  44815  hoicvr  44875  ovnsubaddlem2  44898  hoidmvval0  44914  hoidmvlelem3  44924  hspmbllem2  44954  vonioo  45009  vonicc  45012  smfinflem  45144  fsupdm  45169  finfdm  45173  fmtnoprmfac2lem1  45844  fmtnofac1  45848  lincresunit3lem3  46641  suppdm  46677  inlinecirc02p  46959
  Copyright terms: Public domain W3C validator