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

Theorem mp4an 691
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 471 . 2 (𝜑𝜓)
4 mp4an.3 . . 3 𝜒
5 mp4an.4 . . 3 𝜃
64, 5pm3.2i 471 . 2 (𝜒𝜃)
7 mp4an.5 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
83, 6, 7mp2an 690 1 𝜏
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  noinfep  9592  1lt2nq  10905  m1p1sr  11024  m1m1sr  11025  axi2m1  11091  mul4i  11348  add4i  11375  add42i  11376  addsub4i  11493  muladdi  11602  lt2addi  11713  le2addi  11714  mulne0i  11794  divne0i  11899  divmuldivi  11911  divadddivi  11913  divdivdivi  11914  subreci  11981  8th4div3  12369  xrsup0  13234  fldiv4p1lem1div2  13732  sqrt2gt1lt2  15151  3dvds2dec  16207  flodddiv4  16287  nprmi  16557  mod2xnegi  16935  catcfuccl  17997  catcfucclOLD  17998  catcxpccl  18087  catcxpcclOLD  18088  iccpnfhmeo  24292  xrhmeo  24293  cnheiborlem  24301  pcoval1  24360  pcoval2  24363  pcoass  24371  lhop1lem  25361  efcvx  25792  cos0pilt1  25872  dvrelog  25976  dvlog  25990  dvlog2  25992  dvsqrt  26079  dvcnsqrt  26081  cxpcn3  26085  ang180lem1  26143  dvatan  26269  log2cnv  26278  log2tlbnd  26279  log2ub  26283  harmonicbnd3  26341  ppiub  26536  bposlem8  26623  bposlem9  26624  lgsdir2lem1  26657  m1lgs  26720  2lgslem4  26738  2sqlem11  26761  2sqreultlem  26779  2sqreunnltlem  26782  chebbnd1  26804  0slt1s  27152  usgrexmplef  28093  siilem1  29679  hvadd4i  29886  his35i  29917  bdophsi  30924  bdopcoi  30926  mdcompli  31257  dmdcompli  31258  cshw1s2  31697  xrge00  31760  sqsscirc1  32358  raddcn  32379  xrge0iifcnv  32383  xrge0iifiso  32385  xrge0iifhom  32387  esumcvgsum  32556  dstfrvclim1  32946  signsply0  33032  cvmlift2lem6  33771  cvmlift2lem12  33777  iccioo01  35765  poimirlem9  36054  poimirlem15  36060  sqdeccom12  40741  lhe4.4ex1a  42551  dvcosre  44085  wallispi  44243  fourierdlem57  44336  fourierdlem58  44337  fourierdlem112  44391  fouriersw  44404  2exp340mod341  45857  8exp8mod9  45860  nfermltl8rev  45866  tgblthelfgott  45939  zlmodzxzequa  46509  zlmodzxzequap  46512  sepfsepc  46892
  Copyright terms: Public domain W3C validator