MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp4an Structured version   Unicode version

Theorem mp4an 668
Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)
Hypotheses
Ref Expression
mp4an.1  |-  ph
mp4an.2  |-  ps
mp4an.3  |-  ch
mp4an.4  |-  th
mp4an.5  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
Assertion
Ref Expression
mp4an  |-  ta

Proof of Theorem mp4an
StepHypRef Expression
1 mp4an.1 . . 3  |-  ph
2 mp4an.2 . . 3  |-  ps
31, 2pm3.2i 452 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 452 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 667 1  |-  ta
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  noinfep  7861  1lt2nq  9138  m1p1sr  9255  m1m1sr  9256  axi2m1  9322  mul4i  9562  add4i  9585  addsub4i  9700  muladdi  9791  lt2addi  9898  le2addi  9899  mulne0i  9975  divne0i  10075  divmuldivi  10087  divadddivi  10089  divdivdivi  10090  subreci  10157  8th4div3  10541  xrsup0  11282  sqr2gt1lt2  12760  nprmi  13774  mod2xnegi  14096  catcfuccl  14973  catcxpccl  15013  iccpnfhmeo  20476  xrhmeo  20477  cnheiborlem  20485  pcoval1  20544  pcoval2  20547  pcoass  20555  lhop1lem  21444  efcvx  21873  dvrelog  22041  dvlog  22055  dvlog2  22057  dvsqr  22141  cxpcn3  22145  ang180lem1  22164  dvatan  22289  log2cnv  22298  log2tlbnd  22299  log2ub  22303  harmonicbnd3  22360  ppiub  22502  bposlem8  22589  bposlem9  22590  lgsdir2lem1  22621  m1lgs  22660  2sqlem11  22673  chebbnd1  22680  usgraexmpl  23254  constr3lem4  23468  vdegp1ai  23540  vdegp1bi  23541  siilem1  24186  hvadd4i  24395  his35i  24426  bdophsi  25435  bdopcoi  25437  mdcompli  25768  dmdcompli  25769  xrge00  26080  sqsscirc1  26274  raddcn  26295  xrge0iifcnv  26299  xrge0iifiso  26301  xrge0iifhom  26303  esumfsupre  26456  esumpfinvallem  26459  esumpcvgval  26463  esumcvg  26471  dstfrvclim1  26790  signsply0  26882  cvmlift2lem6  27127  cvmlift2lem12  27133  dvcnsqr  28403  lhe4.4ex1a  29528  dvcosre  29713  wallispi  29790  zlmodzxzequa  30879  zlmodzxzequap  30882
  Copyright terms: Public domain W3C validator