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  4220  rexxfrd  4221  elunirn  5437  onunsnss  6437  snon0  6445  genprndl  6773  genprndu  6774  addlsub  7541  letrp1  7993  peano2uz2  8535  uzind  8539  xrre  8963  xrre2  8964  flqge  9364  monoord  9551  facwordi  9764  facavg  9770  dvdsmultr1  10378  ltoddhalfle  10437  dvdsgcdb  10546  dfgcd2  10547  coprmgcdb  10614  coprmdvds2  10619  exprmfct  10663  prmdvdsfz  10664  prmfac1  10675  rpexp  10676
  Copyright terms: Public domain W3C validator