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  7865  1lt2nq  9142  m1p1sr  9259  m1m1sr  9260  axi2m1  9326  mul4i  9566  add4i  9589  addsub4i  9704  muladdi  9795  lt2addi  9902  le2addi  9903  mulne0i  9979  divne0i  10079  divmuldivi  10091  divadddivi  10093  divdivdivi  10094  subreci  10161  8th4div3  10545  xrsup0  11286  sqr2gt1lt2  12764  nprmi  13778  mod2xnegi  14100  catcfuccl  14977  catcxpccl  15017  iccpnfhmeo  20517  xrhmeo  20518  cnheiborlem  20526  pcoval1  20585  pcoval2  20588  pcoass  20596  lhop1lem  21485  efcvx  21914  dvrelog  22082  dvlog  22096  dvlog2  22098  dvsqr  22182  cxpcn3  22186  ang180lem1  22205  dvatan  22330  log2cnv  22339  log2tlbnd  22340  log2ub  22344  harmonicbnd3  22401  ppiub  22543  bposlem8  22630  bposlem9  22631  lgsdir2lem1  22662  m1lgs  22701  2sqlem11  22714  chebbnd1  22721  usgraexmpl  23319  constr3lem4  23533  vdegp1ai  23605  vdegp1bi  23606  siilem1  24251  hvadd4i  24460  his35i  24491  bdophsi  25500  bdopcoi  25502  mdcompli  25833  dmdcompli  25834  xrge00  26147  sqsscirc1  26338  raddcn  26359  xrge0iifcnv  26363  xrge0iifiso  26365  xrge0iifhom  26367  esumfsupre  26520  esumpfinvallem  26523  esumpcvgval  26527  esumcvg  26535  dstfrvclim1  26860  signsply0  26952  cvmlift2lem6  27197  cvmlift2lem12  27203  dvcnsqr  28478  lhe4.4ex1a  29603  dvcosre  29788  wallispi  29865  zlmodzxzequa  31038  zlmodzxzequap  31041
  Copyright terms: Public domain W3C validator