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

Theorem mp3an2 1303
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an2.1  |-  ps
mp3an2.2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an2  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem mp3an2
StepHypRef Expression
1 mp3an2.1 . 2  |-  ps
2 mp3an2.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expa 1181 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 431 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 962
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 depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  mp3anl2  1310  ordin  4307  ordsuc  4478  omv  6351  oeiv  6352  omv2  6361  1idprl  7405  muladd11  7902  negsub  8017  subneg  8018  ltaddneg  8193  muleqadd  8436  diveqap1  8472  conjmulap  8496  nnsub  8766  addltmul  8963  zltp1le  9115  gtndiv  9153  eluzp1m1  9356  xnn0le2is012  9656  divelunit  9792  fznatpl1  9863  flqbi2  10071  flqdiv  10101  frecfzen2  10207  nn0ennn  10213  faclbnd3  10496  shftfvalg  10597  ovshftex  10598  shftfval  10600  abs2dif  10885  cos2t  11463  sin01gt0  11474  cos01gt0  11475  demoivre  11485  demoivreALT  11486  omeo  11601  gcd0id  11673  sqgcd  11723  isprm3  11805  setscom  12008  setsslid  12018  setsslnid  12019  abssinper  12943
  Copyright terms: Public domain W3C validator