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

Theorem mpan2d 426
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  427  mpan2i  429  ralxfrd  4447  rexxfrd  4448  elunirn  5745  onunsnss  6894  xpfi  6907  snon0  6913  genprndl  7483  genprndu  7484  addlsub  8289  letrp1  8764  peano2uz2  9319  uzind  9323  xrre  9777  xrre2  9778  flqge  10238  monoord  10432  facwordi  10674  facavg  10680  dvdsmultr1  11793  ltoddhalfle  11852  dvdsgcdb  11968  dfgcd2  11969  coprmgcdb  12042  coprmdvds2  12047  exprmfct  12092  prmdvdsfz  12093  prmfac1  12106  rpexp  12107  eulerthlemh  12185  pcpremul  12247  pcdvdsb  12273  pcprmpw2  12286  pockthlem  12308  lgsne0  13733
  Copyright terms: Public domain W3C validator