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

Theorem mpan2d 428
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 258 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpid 42 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  mpand  429  mpan2i  431  ralxfrd  4508  rexxfrd  4509  elunirn  5834  onunsnss  7013  xpfi  7028  snon0  7036  genprndl  7633  genprndu  7634  addlsub  8441  letrp1  8920  peano2uz2  9479  uzind  9483  xrre  9941  xrre2  9942  flqge  10423  monoord  10628  facwordi  10883  facavg  10889  dvdsmultr1  12113  ltoddhalfle  12175  dvdsgcdb  12305  dfgcd2  12306  coprmgcdb  12381  coprmdvds2  12386  exprmfct  12431  prmdvdsfz  12432  prmfac1  12445  rpexp  12446  eulerthlemh  12524  pcpremul  12587  pcdvdsb  12614  pcprmpw2  12627  pockthlem  12650  4sqlem11  12695  lgsne0  15486  gausslemma2dlem1a  15506  gausslemma2dlem2  15510  lgseisenlem1  15518  lgseisenlem2  15519  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  lgsquad2lem1  15529  lgsquad2lem2  15530
  Copyright terms: Public domain W3C validator