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

Theorem mpan2d 419
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mpan2d.1  |-  ( ph  ->  ch )
mpan2d.2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mpan2d  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpan2d
StepHypRef Expression
1 mpan2d.1 . 2  |-  ( ph  ->  ch )
2 mpan2d.2 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32expd 254 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpid 41 1  |-  ( ph  ->  ( ps  ->  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-ia3 106
This theorem is referenced by:  mpand  420  mpan2i  422  ralxfrd  4284  rexxfrd  4285  elunirn  5545  onunsnss  6625  xpfi  6638  snon0  6643  genprndl  7078  genprndu  7079  addlsub  7846  letrp1  8307  peano2uz2  8851  uzind  8855  xrre  9280  xrre2  9281  flqge  9685  monoord  9900  facwordi  10144  facavg  10150  dvdsmultr1  11108  ltoddhalfle  11167  dvdsgcdb  11276  dfgcd2  11277  coprmgcdb  11344  coprmdvds2  11349  exprmfct  11393  prmdvdsfz  11394  prmfac1  11405  rpexp  11406
  Copyright terms: Public domain W3C validator