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

Theorem mp4an 655
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 442 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 442 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 654 1  |-  ta
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  noinfep  7606  1lt2nq  8842  m1p1sr  8959  m1m1sr  8960  axi2m1  9026  mul4i  9255  add4i  9277  addsub4i  9388  muladdi  9476  lt2addi  9581  le2addi  9582  mulne0i  9657  divne0i  9754  divmuldivi  9766  divadddivi  9768  divdivdivi  9769  subreci  9836  8th4div3  10183  xrsup0  10894  sqr2gt1lt2  12072  nprmi  13086  mod2xnegi  13399  catcfuccl  14256  catcxpccl  14296  iccpnfhmeo  18962  xrhmeo  18963  cnheiborlem  18971  pcoval1  19030  pcoval2  19033  pcoass  19041  lhop1lem  19889  efcvx  20357  dvrelog  20520  dvlog  20534  dvlog2  20536  dvsqr  20620  cxpcn3  20624  ang180lem1  20643  dvatan  20767  log2cnv  20776  log2tlbnd  20777  log2ub  20781  harmonicbnd3  20838  ppiub  20980  bposlem8  21067  bposlem9  21068  lgsdir2lem1  21099  m1lgs  21138  2sqlem11  21151  chebbnd1  21158  usgraexmpl  21412  constr3lem4  21626  vdegp1ai  21698  vdegp1bi  21699  siilem1  22344  hvadd4i  22552  his35i  22583  bdophsi  23591  bdopcoi  23593  mdcompli  23924  dmdcompli  23925  xrge00  24200  xrge0adddir  24207  fsumrp0cl  24209  sqsscirc1  24298  raddcn  24307  xrge0iifcnv  24311  xrge0iifiso  24313  xrge0iifhom  24315  lmlimxrge0  24326  rge0scvg  24327  lmdvg  24330  esumfsupre  24453  esumpfinvallem  24456  esumpfinval  24457  esumpfinvalf  24458  esumpcvgval  24460  esumcvg  24468  dstfrvclim1  24727  cvmlift2lem6  24987  cvmlift2lem12  24993  lhe4.4ex1a  27514  dvcosre  27708  wallispi  27786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator