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

Theorem mpd3an3 1301
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 1166 . 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 947
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 949
This theorem is referenced by:  stoic2b  1391  elovmpo  5939  oav  6318  omv  6319  oeiv  6320  f1oeng  6619  mulpipq2  7147  ltrnqg  7196  genipv  7285  subval  7922  subap0  8373  xaddval  9596  fzrevral3  9855  fzoval  9893  subsq2  10368  bcval  10463  dvdsmul1  11442  dvdsmul2  11443  gcdval  11575  eucalgval2  11661  setsvalg  11916  restval  12053  restin  12272  hmeofvalg  12399  cncfval  12655
  Copyright terms: Public domain W3C validator