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

Theorem 3ad2antl1 1119
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 696 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl2 1114 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  smorndom  6630  omeulem1  6825  dif1enOLD  7340  dif1en  7341  ordiso2  7484  infpssrlem4  8186  fin1a2lem9  8288  gchpwdom  8549  tskwun  8659  gruxp  8682  muldvds2  12875  dvds2add  12881  dvds2sub  12882  dvdstr  12883  mulgnnsubcl  14902  mulgpropd  14923  gexdvdsi  15217  rngidss  15690  reslmhm2  16129  issubassa  16383  obs2ss  16956  restntr  17246  cnpnei  17328  upxp  17655  qtopss  17747  opnfbas  17874  fbasrn  17916  trfg  17923  ufilmax  17939  ustuqtop1  18271  prdsxmetlem  18398  nmoix  18763  nmoi2  18764  iimulcl  18962  mbfimaopn2  19549  lgsval4lem  21091  redwlk  21606  gxcl  21853  lnosub  22260  pjspansn  23079  cnpcon  24917  ghomf1olem  25105  nodenselem8  25643  brbtwn2  25844  colinearalg  25849  axsegconlem1  25856  mblfinlem2  26244  mblfinlem3  26245  mettrifi  26463  ghomdiv  26559  grpokerinj  26560  rngohomco  26590  crngohomfo  26616  keridl  26642  mzpsubst  26805  lzunuz  26826  diophrex  26834  rmxycomplete  26980  jm2.26  27073  lnmepi  27160  lmhmlnmsplit  27162  lsslindf  27277  mndvcl  27423  mhmvlin  27429  fmul01lt1  27692  stoweidlem60  27785  wallispilem3  27792  fzo1fzo0n0  28128  vdn1frgrav2  28416  usg2spot2nb  28454  lub0N  29987  glb0N  29991  cvrcon3b  30075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator