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

Theorem mp4an 673
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 455 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 455 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 672 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  8065  1lt2nq  9340  m1p1sr  9458  m1m1sr  9459  axi2m1  9525  mul4i  9765  add4i  9788  addsub4i  9904  muladdi  9996  lt2addi  10104  le2addi  10105  mulne0i  10181  divne0i  10281  divmuldivi  10293  divadddivi  10295  divdivdivi  10296  subreci  10363  8th4div3  10748  xrsup0  11504  sqr2gt1lt2  13058  nprmi  14080  mod2xnegi  14405  catcfuccl  15283  catcxpccl  15323  iccpnfhmeo  21173  xrhmeo  21174  cnheiborlem  21182  pcoval1  21241  pcoval2  21244  pcoass  21252  lhop1lem  22142  efcvx  22571  dvrelog  22739  dvlog  22753  dvlog2  22755  dvsqr  22839  cxpcn3  22843  ang180lem1  22862  dvatan  22987  log2cnv  22996  log2tlbnd  22997  log2ub  23001  harmonicbnd3  23058  ppiub  23200  bposlem8  23287  bposlem9  23288  lgsdir2lem1  23319  m1lgs  23358  2sqlem11  23371  chebbnd1  23378  usgraexmpl  24063  constr3lem4  24309  vdegp1ai  24646  vdegp1bi  24647  siilem1  25428  hvadd4i  25637  his35i  25668  bdophsi  26677  bdopcoi  26679  mdcompli  27010  dmdcompli  27011  xrge00  27322  sqsscirc1  27512  raddcn  27533  xrge0iifcnv  27537  xrge0iifiso  27539  xrge0iifhom  27541  esumfsupre  27703  esumpfinvallem  27706  esumpcvgval  27710  esumcvg  27718  dstfrvclim1  28042  signsply0  28134  cvmlift2lem6  28379  cvmlift2lem12  28385  dvcnsqr  29665  lhe4.4ex1a  30789  sinaover2ne0  31159  dvcosre  31194  wallispi  31325  zlmodzxzequa  32053  zlmodzxzequap  32056
  Copyright terms: Public domain W3C validator