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

Theorem mp2and 429
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 425 . 2 (𝜑 → (𝜒𝜃))
51, 4mpd 13 1 (𝜑𝜃)
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-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  tfisi  4501  tfr0dm  6219  tfr1onlemaccex  6245  tfrcllemaccex  6258  ertrd  6445  th3qlem1  6531  findcard2  6783  findcard2s  6784  diffifi  6788  fimax2gtrilemstep  6794  fidcenumlemrk  6842  fidcenumlemr  6843  isbth  6855  cc2lem  7086  ltbtwnnqq  7235  prarloclemarch2  7239  addlocprlemeqgt  7352  addnqprlemrl  7377  addnqprlemru  7378  mulnqprlemrl  7393  mulnqprlemru  7394  ltexprlemrl  7430  ltexprlemru  7432  addcanprleml  7434  addcanprlemu  7435  recexprlemloc  7451  recexprlem1ssu  7454  cauappcvgprlemladdfl  7475  caucvgprlemloc  7495  caucvgprprlemloccalc  7504  letrd  7898  lelttrd  7899  lttrd  7900  ltletrd  8197  le2addd  8337  le2subd  8338  ltleaddd  8339  leltaddd  8340  lt2subd  8342  ltmul12a  8630  lediv12a  8664  lemul12ad  8712  lemul12bd  8713  lt2halvesd  8979  uzind  9174  uztrn  9354  xrlttrd  9604  xrlelttrd  9605  xrltletrd  9606  xrletrd  9607  ixxss1  9699  ixxss2  9700  ixxss12  9701  fldiv4p1lem1div2  10090  faclbnd3  10501  abs3lemd  10985  xrbdtri  11057  modfsummod  11239  mertenslemi1  11316  sin01gt0  11479  cos01gt0  11480  sin02gt0  11481  dvds2subd  11540  zsupcllemex  11650  zssinfcl  11652  bezoutlemstep  11696  mulgcd  11715  gcddvdslcm  11765  lcmgcdeq  11775  mulgcddvds  11786  rpmulgcd2  11787  rpdvds  11791  divgcdcoprmex  11794  rpexp  11842  phimullem  11912  exmidunben  11950  lmtopcnp  12433  blin2  12615  xmetxp  12690  tgqioo  12730  cncfmptid  12766  negcncf  12771  limcimolemlt  12816  sinq12gt0  12933  logdivlti  12981
  Copyright terms: Public domain W3C validator