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

Theorem mpd3an3 1320
Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
Hypotheses
Ref Expression
mpd3an3.2  |-  ( (
ph  /\  ps )  ->  ch )
mpd3an3.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mpd3an3  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem mpd3an3
StepHypRef Expression
1 mpd3an3.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 mpd3an3.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expa 1185 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpdan 418 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 963
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 965
This theorem is referenced by:  stoic2b  1410  elovmpo  6021  oav  6401  omv  6402  oeiv  6403  f1oeng  6702  mulpipq2  7291  ltrnqg  7340  genipv  7429  subval  8067  subap0  8518  xaddval  9749  fzrevral3  10009  fzoval  10047  subsq2  10526  bcval  10623  dvdsmul1  11709  dvdsmul2  11710  gcdval  11843  eucalgval2  11930  setsvalg  12231  restval  12368  restin  12587  hmeofvalg  12714  cncfval  12970  rpcxpef  13226  rpcxpneg  13239
  Copyright terms: Public domain W3C validator