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

Theorem mpanr2 688
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpanr2.1  |-  ch
mpanr2.2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
mpanr2  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem mpanr2
StepHypRef Expression
1 mpanr2.1 . . 3  |-  ch
21jctr 544 . 2  |-  ( ps 
->  ( ps  /\  ch ) )
3 mpanr2.2 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
42, 3sylan2 476 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  fvreseq1  5998  op1steq  6849  fpmg  7505  pmresg  7507  pw2f1o  7683  pm54.43  8433  dfac2  8559  ttukeylem6  8942  gruina  9242  muleqadd  10255  divdiv1  10317  addltmul  10848  elfzp1b  11869  elfzm1b  11870  expp1z  12318  expm1  12319  oddvdsnn0  17135  efgi0  17305  efgi1  17306  fiinbas  19898  opnneissb  20061  fclscf  20971  blssec  21381  iimulcl  21861  itg2lr  22565  blocnilem  26290  lnopmul  27455  opsqrlem6  27633  gsumle  28380  gsumvsca1  28384  gsumvsca2  28385  locfinreflem  28506  fvray  30693  fvline  30696  fneref  30791  poimirlem3  31647  poimirlem16  31660  fdc  31778  linepmap  33049  rmyeq0  35509
  Copyright terms: Public domain W3C validator