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

Theorem mp2and 424
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 420 . 2 (𝜑 → (𝜒𝜃))
51, 4mpd 13 1 (𝜑𝜃)
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  4356  tfr0dm  5991  tfr1onlemaccex  6017  tfrcllemaccex  6030  ertrd  6209  th3qlem1  6295  findcard2  6445  findcard2s  6446  diffifi  6450  ltbtwnnqq  6719  prarloclemarch2  6723  addlocprlemeqgt  6836  addnqprlemrl  6861  addnqprlemru  6862  mulnqprlemrl  6877  mulnqprlemru  6878  ltexprlemrl  6914  ltexprlemru  6916  addcanprleml  6918  addcanprlemu  6919  recexprlemloc  6935  recexprlem1ssu  6938  cauappcvgprlemladdfl  6959  caucvgprlemloc  6979  caucvgprprlemloccalc  6988  letrd  7352  lelttrd  7353  lttrd  7354  ltletrd  7646  le2addd  7782  le2subd  7783  ltleaddd  7784  leltaddd  7785  lt2subd  7787  ltmul12a  8057  lediv12a  8091  lemul12ad  8139  lemul12bd  8140  lt2halvesd  8397  uzind  8591  uztrn  8768  xrlttrd  9007  xrlelttrd  9008  xrltletrd  9009  xrletrd  9010  ixxss1  9055  ixxss2  9056  ixxss12  9057  fldiv4p1lem1div2  9439  faclbnd3  9819  abs3lemd  10288  dvds2subd  10439  zsupcllemex  10549  zssinfcl  10551  bezoutlemstep  10593  mulgcd  10612  gcddvdslcm  10662  lcmgcdeq  10672  mulgcddvds  10683  rpmulgcd2  10684  rpdvds  10688  divgcdcoprmex  10691  rpexp  10739  phimullem  10808
  Copyright terms: Public domain W3C validator