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

Theorem mpanl12 434
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 432 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 422 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  reuun1  3409  ordtri2orexmid  4505  opthreg  4538  ordtri2or2exmid  4553  ontri2orexmidim  4554  fvtp1  5704  nq0m0r  7405  nq02m  7414  gt0srpr  7697  map2psrprg  7754  pitoregt0  7798  axcnre  7830  addgt0  8354  addgegt0  8355  addgtge0  8356  addge0  8357  addgt0i  8394  addge0i  8395  addgegt0i  8396  add20i  8398  mulge0i  8526  recextlem1  8556  recap0  8589  recdivap  8622  recgt1  8800  prodgt0i  8811  prodge0i  8812  iccshftri  9939  iccshftli  9941  iccdili  9943  icccntri  9945  mulexpzap  10503  expaddzap  10507  m1expeven  10510  iexpcyc  10567  amgm2  11069  ege2le3  11621  sqnprm  12077  lmres  12963  2logb9irrap  13610
  Copyright terms: Public domain W3C validator