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  3262  ordtri2orexmid  4294  opthreg  4327  ordtri2or2exmid  4342  fvtp1  5424  nq0m0r  6760  nq02m  6769  gt0srpr  7039  pitoregt0  7131  axcnre  7161  addgt0  7671  addgegt0  7672  addgtge0  7673  addge0  7674  addgt0i  7708  addge0i  7709  addgegt0i  7710  add20i  7712  mulge0i  7839  recextlem1  7860  recap0  7892  recdivap  7925  recgt1  8094  prodgt0i  8105  prodge0i  8106  iccshftri  9145  iccshftli  9147  iccdili  9149  icccntri  9151  mulexpzap  9665  expaddzap  9669  m1expeven  9672  iexpcyc  9728  amgm2  10205  sqnprm  10724
  Copyright terms: Public domain W3C validator