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

Theorem 3adant3r2 1163
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 1154 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1117 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:  plttr  14386  latjlej2  14454  latmlem1  14469  latmlem2  14470  latledi  14477  latmlej11  14478  latmlej12  14479  ipopos  14545  grppnpcan2  14841  mulgsubdir  14880  imasrng  15684  zntoslem  16796  mettri2  18328  mettri  18339  xmetrtri  18342  xmetrtri2  18343  metrtri  18344  grpopnpcan2  21798  grponnncan2  21799  ablomuldiv  21834  ablonnncan1  21840  nvmdi  22088  dipdi  22301  dipassr  22304  dipsubdir  22306  dipsubdi  22307  btwncomim  25855  cgr3tr4  25894  cgr3rflx  25896  colinbtwnle  25960  rngosubdi  26463  rngosubdir  26464  dmncan1  26580  dmncan2  26581  mendlmod  27373  omlfh1N  29745  omlfh3N  29746  cvrnbtwn3  29763  cvrnbtwn4  29766  cvrcmp2  29771  hlatjrot  29859  cvrat3  29928  lplnribN  30037  ltrn2ateq  30666  dvalveclem  31512
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