ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpanr2 Unicode version

Theorem mpanr2 432
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 311 . 2  |-  ( ps 
->  ( ps  /\  ch ) )
3 mpanr2.2 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
42, 3sylan2 282 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  op1steq  6007  fpmg  6498  pmresg  6500  pm54.43  6957  prarloclemarch2  7128  prarloclemlt  7202  prsradd  7481  muleqadd  8290  divdivap1  8344  addltmul  8808  elfzp1b  9718  elfzm1b  9719  expp1zap  10183  expm1ap  10184  fiinbas  11998  opnneissb  12106  blssec  12366
  Copyright terms: Public domain W3C validator