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  4507  opthreg  4540  ordtri2or2exmid  4555  ontri2orexmidim  4556  fvtp1  5707  nq0m0r  7418  nq02m  7427  gt0srpr  7710  map2psrprg  7767  pitoregt0  7811  axcnre  7843  addgt0  8367  addgegt0  8368  addgtge0  8369  addge0  8370  addgt0i  8407  addge0i  8408  addgegt0i  8409  add20i  8411  mulge0i  8539  recextlem1  8569  recap0  8602  recdivap  8635  recgt1  8813  prodgt0i  8824  prodge0i  8825  iccshftri  9952  iccshftli  9954  iccdili  9956  icccntri  9958  mulexpzap  10516  expaddzap  10520  m1expeven  10523  iexpcyc  10580  amgm2  11082  ege2le3  11634  sqnprm  12090  lmres  13042  2logb9irrap  13689
  Copyright terms: Public domain W3C validator