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

Theorem mp2and 424
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2and.1  |-  ( ph  ->  ps )
mp2and.2  |-  ( ph  ->  ch )
mp2and.3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mp2and  |-  ( ph  ->  th )

Proof of Theorem mp2and
StepHypRef Expression
1 mp2and.2 . 2  |-  ( ph  ->  ch )
2 mp2and.1 . . 3  |-  ( ph  ->  ps )
3 mp2and.3 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
42, 3mpand 420 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 13 1  |-  ( ph  ->  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-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  tfisi  4402  tfr0dm  6087  tfr1onlemaccex  6113  tfrcllemaccex  6126  ertrd  6306  th3qlem1  6392  findcard2  6603  findcard2s  6604  diffifi  6608  fimax2gtrilemstep  6614  fidcenumlemrk  6661  fidcenumlemr  6662  isbth  6674  ltbtwnnqq  6972  prarloclemarch2  6976  addlocprlemeqgt  7089  addnqprlemrl  7114  addnqprlemru  7115  mulnqprlemrl  7130  mulnqprlemru  7131  ltexprlemrl  7167  ltexprlemru  7169  addcanprleml  7171  addcanprlemu  7172  recexprlemloc  7188  recexprlem1ssu  7191  cauappcvgprlemladdfl  7212  caucvgprlemloc  7232  caucvgprprlemloccalc  7241  letrd  7605  lelttrd  7606  lttrd  7607  ltletrd  7899  le2addd  8038  le2subd  8039  ltleaddd  8040  leltaddd  8041  lt2subd  8043  ltmul12a  8319  lediv12a  8353  lemul12ad  8401  lemul12bd  8402  lt2halvesd  8661  uzind  8855  uztrn  9033  xrlttrd  9272  xrlelttrd  9273  xrltletrd  9274  xrletrd  9275  ixxss1  9320  ixxss2  9321  ixxss12  9322  fldiv4p1lem1div2  9708  faclbnd3  10147  abs3lemd  10630  modfsummod  10848  mertenslemi1  10925  sin01gt0  11048  cos01gt0  11049  sin02gt0  11050  dvds2subd  11106  zsupcllemex  11216  zssinfcl  11218  bezoutlemstep  11260  mulgcd  11279  gcddvdslcm  11329  lcmgcdeq  11339  mulgcddvds  11350  rpmulgcd2  11351  rpdvds  11355  divgcdcoprmex  11358  rpexp  11406  phimullem  11475
  Copyright terms: Public domain W3C validator