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

Theorem mpan2d 425
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  426  mpan2i  428  ralxfrd  4424  rexxfrd  4425  elunirn  5718  onunsnss  6863  xpfi  6876  snon0  6882  genprndl  7443  genprndu  7444  addlsub  8249  letrp1  8724  peano2uz2  9276  uzind  9280  xrre  9730  xrre2  9731  flqge  10190  monoord  10384  facwordi  10625  facavg  10631  dvdsmultr1  11737  ltoddhalfle  11796  dvdsgcdb  11912  dfgcd2  11913  coprmgcdb  11980  coprmdvds2  11985  exprmfct  12030  prmdvdsfz  12031  prmfac1  12042  rpexp  12043  eulerthlemh  12121  pcpremul  12183
  Copyright terms: Public domain W3C validator