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

Theorem 3adant3r2 1206
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 1197 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
323adantr2 1156 1  |-  ( (
ph  /\  ( ps  /\ 
ta  /\  ch )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  plttr  15460  latjlej2  15556  latmlem1  15571  latmlem2  15572  latledi  15579  latmlej11  15580  latmlej12  15581  ipopos  15650  grppnpcan2  15946  mulgsubdir  15987  imasrng  17081  zntoslem  18402  mettri2  20671  mettri  20682  xmetrtri  20685  xmetrtri2  20686  metrtri  20687  grpopnpcan2  25028  grponnncan2  25029  ablomuldiv  25064  ablonnncan1  25070  nvmdi  25318  dipdi  25531  dipassr  25534  dipsubdir  25536  dipsubdi  25537  btwncomim  29516  cgr3tr4  29555  cgr3rflx  29557  colinbtwnle  29621  rngosubdi  30186  rngosubdir  30187  dmncan1  30303  dmncan2  30304  mendlmod  30974  omlfh1N  34272  omlfh3N  34273  cvrnbtwn3  34290  cvrnbtwn4  34293  cvrcmp2  34298  hlatjrot  34386  cvrat3  34455  lplnribN  34564  ltrn2ateq  35193  dvalveclem  36039
  Copyright terms: Public domain W3C validator