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

Theorem 3ad2antl1 1157
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 1152 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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 974
This theorem is referenced by:  smorndom  7037  omeulem1  7229  dif1enOLD  7750  dif1en  7751  ordiso2  7938  infpssrlem4  8684  fin1a2lem9  8786  gchpwdom  9046  tskwun  9160  gruxp  9183  fzo1fzo0n0  11838  fsuppmapnn0fiub  12071  muldvds2  13881  dvds2add  13887  dvds2sub  13888  dvdstr  13890  mulgnnsubcl  16023  mulgpropd  16044  gexdvdsi  16472  ringidss  17093  reslmhm2  17567  issubassa  17841  obs2ss  18627  lsslindf  18732  mndvcl  18760  mhmvlin  18766  madurid  19013  restntr  19549  cnpnei  19631  upxp  19990  qtopss  20082  opnfbas  20209  fbasrn  20251  trfg  20258  ufilmax  20274  ustuqtop1  20610  prdsxmetlem  20737  nmoix  21102  nmoi2  21103  iimulcl  21303  mbfimaopn2  21930  lgsval4lem  23447  f1otrg  24039  brbtwn2  24073  colinearalg  24078  axsegconlem1  24085  redwlk  24473  vdn1frgrav2  24890  usg2spot2nb  24930  numclwlk1lem2fo  24960  gxcl  25132  lnosub  25539  pjspansn  26360  eulerpartlemb  28173  cnpcon  28541  mclspps  28810  ghomf1olem  28900  nodenselem8  29416  mblfinlem2  30020  mblfinlem3  30021  mettrifi  30218  ghomdiv  30314  grpokerinj  30315  rngohomco  30345  crngohomfo  30371  keridl  30397  mzpsubst  30649  lzunuz  30669  diophrex  30677  rmxycomplete  30821  jm2.26  30912  lnmepi  30999  lmhmlnmsplit  31001  fmul01lt1  31504  limcleqr  31554  limclner  31561  volioc  31657  stoweidlem60  31727  wallispilem3  31734  fourierdlem12  31786  fourierdlem41  31815  fourierdlem42  31816  fourierdlem48  31822  fourierdlem49  31823  fourierdlem54  31828  fourierdlem68  31842  fourierdlem73  31847  fourierdlem74  31848  fourierdlem75  31849  fourierdlem83  31857  lincresunit3lem3  32785  cvrcon3b  34704
  Copyright terms: Public domain W3C validator