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

Theorem mp2and 409
 Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2and.1
mp2and.2
mp2and.3
Assertion
Ref Expression
mp2and

Proof of Theorem mp2and
StepHypRef Expression
1 mp2and.2 . 2
2 mp2and.1 . . 3
3 mp2and.3 . . 3
42, 3mpand 405 . 2
51, 4mpd 13 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  ssnelpssd  3290  tfisi  4310  tfr0  5937  ertrd  6122  th3qlem1  6208  findcard2  6346  findcard2s  6347  diffifi  6351  ltbtwnnqq  6513  prarloclemarch2  6517  addlocprlemeqgt  6630  addnqprlemrl  6655  addnqprlemru  6656  mulnqprlemrl  6671  mulnqprlemru  6672  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  recexprlemloc  6729  recexprlem1ssu  6732  cauappcvgprlemladdfl  6753  caucvgprlemloc  6773  caucvgprprlemloccalc  6782  letrd  7138  lelttrd  7139  lttrd  7140  ltletrd  7420  le2addd  7554  le2subd  7555  ltleaddd  7556  leltaddd  7557  lt2subd  7559  ltmul12a  7826  lediv12a  7860  lemul12ad  7908  lemul12bd  7909  lt2halvesd  8172  uzind  8349  uztrn  8489  xrlttrd  8725  xrlelttrd  8726  xrltletrd  8727  xrletrd  8728  ixxss1  8773  ixxss2  8774  ixxss12  8775  fldiv4p1lem1div2  9147  abs3lemd  9797
 Copyright terms: Public domain W3C validator