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

Theorem mpan2d 424
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 256 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpid 42 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  mpand  425  mpan2i  427  ralxfrd  4383  rexxfrd  4384  elunirn  5667  onunsnss  6805  xpfi  6818  snon0  6824  genprndl  7336  genprndu  7337  addlsub  8139  letrp1  8613  peano2uz2  9165  uzind  9169  xrre  9610  xrre2  9611  flqge  10062  monoord  10256  facwordi  10493  facavg  10499  dvdsmultr1  11538  ltoddhalfle  11597  dvdsgcdb  11708  dfgcd2  11709  coprmgcdb  11776  coprmdvds2  11781  exprmfct  11825  prmdvdsfz  11826  prmfac1  11837  rpexp  11838
  Copyright terms: Public domain W3C validator