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

Theorem 3ad2antl1 1153
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antl1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3ad2antl1
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantlr 714 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl2 1148 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 185  df-an 371  df-3an 970
This theorem is referenced by:  smorndom  7029  omeulem1  7221  dif1enOLD  7741  dif1en  7742  ordiso2  7929  infpssrlem4  8675  fin1a2lem9  8777  gchpwdom  9037  tskwun  9151  gruxp  9174  fzo1fzo0n0  11821  fsuppmapnn0fiub  12053  muldvds2  13859  dvds2add  13865  dvds2sub  13866  dvdstr  13867  mulgnnsubcl  15947  mulgpropd  15968  gexdvdsi  16392  rngidss  17005  reslmhm2  17475  issubassa  17737  obs2ss  18520  lsslindf  18625  mndvcl  18653  mhmvlin  18659  madurid  18906  restntr  19442  cnpnei  19524  upxp  19852  qtopss  19944  opnfbas  20071  fbasrn  20113  trfg  20120  ufilmax  20136  ustuqtop1  20472  prdsxmetlem  20599  nmoix  20964  nmoi2  20965  iimulcl  21165  mbfimaopn2  21792  lgsval4lem  23303  f1otrg  23843  brbtwn2  23877  colinearalg  23882  axsegconlem1  23889  redwlk  24270  vdn1frgrav2  24688  usg2spot2nb  24728  numclwlk1lem2fo  24758  gxcl  24929  lnosub  25336  pjspansn  26157  eulerpartlemb  27933  cnpcon  28301  ghomf1olem  28495  nodenselem8  29011  mblfinlem2  29616  mblfinlem3  29617  mettrifi  29840  ghomdiv  29936  grpokerinj  29937  rngohomco  29967  crngohomfo  29993  keridl  30019  mzpsubst  30272  lzunuz  30292  diophrex  30300  rmxycomplete  30444  jm2.26  30537  lnmepi  30624  lmhmlnmsplit  30626  fmul01lt1  31091  limcleqr  31141  limclner  31148  volioc  31245  stoweidlem60  31315  wallispilem3  31322  fourierdlem12  31374  fourierdlem41  31403  fourierdlem42  31404  fourierdlem48  31410  fourierdlem49  31411  fourierdlem54  31416  fourierdlem68  31430  fourierdlem73  31435  fourierdlem74  31436  fourierdlem75  31437  fourierdlem83  31445  lincresunit3lem3  32023  cvrcon3b  33949
  Copyright terms: Public domain W3C validator