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

Theorem mp4an 711
Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)
Hypotheses
Ref Expression
mp4an.1 𝜑
mp4an.2 𝜓
mp4an.3 𝜒
mp4an.4 𝜃
mp4an.5 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
mp4an 𝜏

Proof of Theorem mp4an
StepHypRef Expression
1 mp4an.1 . . 3 𝜑
2 mp4an.2 . . 3 𝜓
31, 2pm3.2i 470 . 2 (𝜑𝜓)
4 mp4an.3 . . 3 𝜒
5 mp4an.4 . . 3 𝜃
64, 5pm3.2i 470 . 2 (𝜒𝜃)
7 mp4an.5 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
83, 6, 7mp2an 710 1 𝜏
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  noinfep  8730  1lt2nq  9987  m1p1sr  10105  m1m1sr  10106  axi2m1  10172  mul4i  10425  add4i  10452  add42i  10453  addsub4i  10569  muladdi  10673  lt2addi  10782  le2addi  10783  mulne0i  10862  divne0i  10965  divmuldivi  10977  divadddivi  10979  divdivdivi  10980  subreci  11047  8th4div3  11444  xrsup0  12346  fldiv4p1lem1div2  12830  sqrt2gt1lt2  14214  3dvds2dec  15258  3dvds2decOLD  15259  flodddiv4  15339  nprmi  15604  mod2xnegi  15977  catcfuccl  16960  catcxpccl  17048  iccpnfhmeo  22945  xrhmeo  22946  cnheiborlem  22954  pcoval1  23013  pcoval2  23016  pcoass  23024  lhop1lem  23975  efcvx  24402  dvrelog  24582  dvlog  24596  dvlog2  24598  dvsqrt  24682  dvcnsqrt  24684  cxpcn3  24688  ang180lem1  24738  dvatan  24861  log2cnv  24870  log2tlbnd  24871  log2ub  24875  harmonicbnd3  24933  ppiub  25128  bposlem8  25215  bposlem9  25216  lgsdir2lem1  25249  m1lgs  25312  2lgslem4  25330  2sqlem11  25353  chebbnd1  25360  usgrexmplef  26350  siilem1  28015  hvadd4i  28224  his35i  28255  bdophsi  29264  bdopcoi  29266  mdcompli  29597  dmdcompli  29598  xrge00  29995  sqsscirc1  30263  raddcn  30284  xrge0iifcnv  30288  xrge0iifiso  30290  xrge0iifhom  30292  esumcvgsum  30459  dstfrvclim1  30848  signsply0  30937  cvmlift2lem6  31597  cvmlift2lem12  31603  poimirlem9  33731  poimirlem15  33737  lhe4.4ex1a  39030  dvcosre  40629  wallispi  40790  fourierdlem57  40883  fourierdlem58  40884  fourierdlem112  40938  fouriersw  40951  tgblthelfgott  42213  tgblthelfgottOLD  42219  zlmodzxzequa  42795  zlmodzxzequap  42798
  Copyright terms: Public domain W3C validator