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

Theorem mp4an 671
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 453 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 453 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 670 1  |-  ta
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  noinfep  8108  1lt2nq  9380  m1p1sr  9498  m1m1sr  9499  axi2m1  9565  mul4i  9810  add4i  9833  add42i  9834  addsub4i  9951  muladdi  10047  lt2addi  10154  le2addi  10155  mulne0i  10232  divne0i  10332  divmuldivi  10344  divadddivi  10346  divdivdivi  10347  subreci  10414  8th4div3  10799  xrsup0  11567  sqrt2gt1lt2  13255  nprmi  14439  mod2xnegi  14764  catcfuccl  15710  catcxpccl  15798  iccpnfhmeo  21735  xrhmeo  21736  cnheiborlem  21744  pcoval1  21803  pcoval2  21806  pcoass  21814  lhop1lem  22704  efcvx  23134  dvrelog  23310  dvlog  23324  dvlog2  23326  dvsqrt  23410  dvcnsqrt  23412  cxpcn3  23416  ang180lem1  23466  dvatan  23589  log2cnv  23598  log2tlbnd  23599  log2ub  23603  harmonicbnd3  23661  ppiub  23858  bposlem8  23945  bposlem9  23946  lgsdir2lem1  23977  m1lgs  24016  2sqlem11  24029  chebbnd1  24036  usgraexmpl  24805  constr3lem4  25051  vdegp1ai  25388  vdegp1bi  25389  siilem1  26166  hvadd4i  26375  his35i  26406  bdophsi  27414  bdopcoi  27416  mdcompli  27747  dmdcompli  27748  xrge00  28112  sqsscirc1  28329  raddcn  28350  xrge0iifcnv  28354  xrge0iifiso  28356  xrge0iifhom  28358  esumcvgsum  28521  dstfrvclim1  28908  signsply0  29000  cvmlift2lem6  29592  cvmlift2lem12  29598  lhe4.4ex1a  36062  dvcosre  37055  wallispi  37201  fourierdlem57  37295  fourierdlem58  37296  fourierdlem112  37350  fouriersw  37363  zlmodzxzequa  38589  zlmodzxzequap  38592
  Copyright terms: Public domain W3C validator