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

Theorem 3adant3r2 1161
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant3r2  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )

Proof of Theorem 3adant3r2
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1152 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1115 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  plttr  14104  latjlej2  14172  latmlem1  14187  latmlem2  14188  latledi  14195  latmlej11  14196  latmlej12  14197  ipopos  14263  grppnpcan2  14559  mulgsubdir  14598  imasrng  15402  zntoslem  16510  mettri2  17906  mettri  17916  xmetrtri  17919  xmetrtri2  17920  metrtri  17921  grpopnpcan2  20920  grponnncan2  20921  ablomuldiv  20956  ablonnncan1  20962  nvmdi  21208  dipdi  21421  dipassr  21424  dipsubdir  21426  dipsubdi  21427  btwncomim  24636  cgr3tr4  24675  cgr3rflx  24677  colinbtwnle  24741  grpodrcan  25375  homgrf  25802  rngosubdi  26584  rngosubdir  26585  dmncan1  26701  dmncan2  26702  mendlmod  27501  omlfh1N  29448  omlfh3N  29449  cvrnbtwn3  29466  cvrnbtwn4  29469  cvrcmp2  29474  hlatjrot  29562  cvrat3  29631  lplnribN  29740  ltrn2ateq  30369  dvalveclem  31215
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator