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

Theorem mp4an 654
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 441 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 441 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 653 1  |-  ta
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  noinfep  7376  1lt2nq  8613  m1p1sr  8730  m1m1sr  8731  axi2m1  8797  mul4i  9025  add4i  9047  addsub4i  9158  muladdi  9246  lt2addi  9351  le2addi  9352  mulne0i  9427  divne0i  9524  divmuldivi  9536  divadddivi  9538  divdivdivi  9539  subreci  9606  8th4div3  9951  xrsup0  10658  sqr2gt1lt2  11776  nprmi  12789  mod2xnegi  13102  catcfuccl  13957  catcxpccl  13997  iccpnfhmeo  18459  xrhmeo  18460  cnheiborlem  18468  pcoval1  18527  pcoval2  18530  pcoass  18538  lhop1lem  19376  efcvx  19841  dvrelog  20000  dvlog  20014  dvlog2  20016  dvsqr  20100  cxpcn3  20104  ang180lem1  20123  dvatan  20247  log2cnv  20256  log2tlbnd  20257  log2ub  20261  harmonicbnd3  20317  ppiub  20459  bposlem8  20546  bposlem9  20547  lgsdir2lem1  20578  m1lgs  20617  2sqlem11  20630  chebbnd1  20637  siilem1  21445  hvadd4i  21653  his35i  21684  bdophsi  22692  bdopcoi  22694  mdcompli  23025  dmdcompli  23026  sqsscirc1  23307  raddcn  23317  xrge00  23326  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhom  23334  xrge0adddir  23347  fsumrp0cl  23349  lmlimxrge0  23387  rge0scvg  23388  lmdvg  23391  esumpfinvallem  23457  esumpfinval  23458  esumpfinvalf  23459  esumpcvgval  23461  esumcvg  23469  dstfrvclim1  23693  cvmlift2lem6  23854  cvmlift2lem12  23860  vdegp1ai  23923  vdegp1bi  23924  domrancur1b  25303  mp4anOLD  26439  lhe4.4ex1a  27649  usgraexmpl  28267  constr3lem4  28393
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 177  df-an 360
  Copyright terms: Public domain W3C validator