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

Theorem mp2and 417
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 413 . 2 (𝜑 → (𝜒𝜃))
51, 4mpd 13 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  ssnelpssd  3317  tfisi  4337  tfr0  5967  ertrd  6152  th3qlem1  6238  findcard2  6376  findcard2s  6377  diffifi  6381  ltbtwnnqq  6570  prarloclemarch2  6574  addlocprlemeqgt  6687  addnqprlemrl  6712  addnqprlemru  6713  mulnqprlemrl  6728  mulnqprlemru  6729  ltexprlemrl  6765  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  recexprlemloc  6786  recexprlem1ssu  6789  cauappcvgprlemladdfl  6810  caucvgprlemloc  6830  caucvgprprlemloccalc  6839  letrd  7198  lelttrd  7199  lttrd  7200  ltletrd  7491  le2addd  7627  le2subd  7628  ltleaddd  7629  leltaddd  7630  lt2subd  7632  ltmul12a  7900  lediv12a  7934  lemul12ad  7982  lemul12bd  7983  lt2halvesd  8228  uzind  8407  uztrn  8584  xrlttrd  8825  xrlelttrd  8826  xrltletrd  8827  xrletrd  8828  ixxss1  8873  ixxss2  8874  ixxss12  8875  fldiv4p1lem1div2  9249  faclbnd3  9604  abs3lemd  10020  dvds2subd  10135
  Copyright terms: Public domain W3C validator