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

Theorem mpd3an3 1316
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 1181 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpdan 417 1  |-  ( (
ph  /\  ps )  ->  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:  stoic2b  1406  elovmpo  5964  oav  6343  omv  6344  oeiv  6345  f1oeng  6644  mulpipq2  7172  ltrnqg  7221  genipv  7310  subval  7947  subap0  8398  xaddval  9621  fzrevral3  9880  fzoval  9918  subsq2  10393  bcval  10488  dvdsmul1  11504  dvdsmul2  11505  gcdval  11637  eucalgval2  11723  setsvalg  11978  restval  12115  restin  12334  hmeofvalg  12461  cncfval  12717
  Copyright terms: Public domain W3C validator