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

Theorem mpanl12 427
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mpanl12.1  |-  ph
mpanl12.2  |-  ps
mpanl12.3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
mpanl12  |-  ( ch 
->  th )

Proof of Theorem mpanl12
StepHypRef Expression
1 mpanl12.2 . 2  |-  ps
2 mpanl12.1 . . 3  |-  ph
3 mpanl12.3 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3mpanl1 425 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 415 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  reuun1  3281  ordtri2orexmid  4339  opthreg  4372  ordtri2or2exmid  4387  fvtp1  5508  nq0m0r  7015  nq02m  7024  gt0srpr  7294  pitoregt0  7386  axcnre  7416  addgt0  7926  addgegt0  7927  addgtge0  7928  addge0  7929  addgt0i  7966  addge0i  7967  addgegt0i  7968  add20i  7970  mulge0i  8097  recextlem1  8120  recap0  8152  recdivap  8185  recgt1  8358  prodgt0i  8369  prodge0i  8370  iccshftri  9412  iccshftli  9414  iccdili  9416  icccntri  9418  mulexpzap  9995  expaddzap  9999  m1expeven  10002  iexpcyc  10059  amgm2  10551  ege2le3  10961  sqnprm  11395
  Copyright terms: Public domain W3C validator