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  7360  1lt2nq  8597  m1p1sr  8714  m1m1sr  8715  axi2m1  8781  mul4i  9009  add4i  9031  addsub4i  9142  muladdi  9230  lt2addi  9335  le2addi  9336  mulne0i  9411  divne0i  9508  divmuldivi  9520  divadddivi  9522  divdivdivi  9523  subreci  9590  8th4div3  9935  xrsup0  10642  sqr2gt1lt2  11760  nprmi  12773  mod2xnegi  13086  catcfuccl  13941  catcxpccl  13981  iccpnfhmeo  18443  xrhmeo  18444  cnheiborlem  18452  pcoval1  18511  pcoval2  18514  pcoass  18522  lhop1lem  19360  efcvx  19825  dvrelog  19984  dvlog  19998  dvlog2  20000  dvsqr  20084  cxpcn3  20088  ang180lem1  20107  dvatan  20231  log2cnv  20240  log2tlbnd  20241  log2ub  20245  harmonicbnd3  20301  ppiub  20443  bposlem8  20530  bposlem9  20531  lgsdir2lem1  20562  m1lgs  20601  2sqlem11  20614  chebbnd1  20621  siilem1  21429  hvadd4i  21637  his35i  21668  bdophsi  22676  bdopcoi  22678  mdcompli  23009  dmdcompli  23010  sqsscirc1  23292  raddcn  23302  xrge00  23311  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  xrge0adddir  23332  fsumrp0cl  23334  lmlimxrge0  23372  rge0scvg  23373  lmdvg  23376  esumpfinvallem  23442  esumpfinval  23443  esumpfinvalf  23444  esumpcvgval  23446  esumcvg  23454  dstfrvclim1  23678  cvmlift2lem6  23839  cvmlift2lem12  23845  vdegp1ai  23908  vdegp1bi  23909  domrancur1b  25200  mp4anOLD  26336  lhe4.4ex1a  27546  usgraexmpl  28133
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