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

Theorem mp4an 689
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 688 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 208  df-an 397
This theorem is referenced by:  noinfep  9112  1lt2nq  10384  m1p1sr  10503  m1m1sr  10504  axi2m1  10570  mul4i  10826  add4i  10853  add42i  10854  addsub4i  10971  muladdi  11080  lt2addi  11191  le2addi  11192  mulne0i  11272  divne0i  11377  divmuldivi  11389  divadddivi  11391  divdivdivi  11392  subreci  11459  8th4div3  11846  xrsup0  12706  fldiv4p1lem1div2  13195  sqrt2gt1lt2  14624  3dvds2dec  15672  flodddiv4  15754  nprmi  16023  mod2xnegi  16397  catcfuccl  17359  catcxpccl  17447  iccpnfhmeo  23478  xrhmeo  23479  cnheiborlem  23487  pcoval1  23546  pcoval2  23549  pcoass  23557  lhop1lem  24539  efcvx  24966  dvrelog  25147  dvlog  25161  dvlog2  25163  dvsqrt  25250  dvcnsqrt  25252  cxpcn3  25256  ang180lem1  25314  dvatan  25440  log2cnv  25450  log2tlbnd  25451  log2ub  25455  harmonicbnd3  25513  ppiub  25708  bposlem8  25795  bposlem9  25796  lgsdir2lem1  25829  m1lgs  25892  2lgslem4  25910  2sqlem11  25933  2sqreultlem  25951  2sqreunnltlem  25954  chebbnd1  25976  usgrexmplef  26969  siilem1  28556  hvadd4i  28763  his35i  28794  bdophsi  29801  bdopcoi  29803  mdcompli  30134  dmdcompli  30135  cshw1s2  30562  xrge00  30601  sqsscirc1  31051  raddcn  31072  xrge0iifcnv  31076  xrge0iifiso  31078  xrge0iifhom  31080  esumcvgsum  31247  dstfrvclim1  31635  signsply0  31721  cvmlift2lem6  32453  cvmlift2lem12  32459  poimirlem9  34783  poimirlem15  34789  sqdeccom12  39055  lhe4.4ex1a  40541  dvcosre  42076  wallispi  42236  fourierdlem57  42329  fourierdlem58  42330  fourierdlem112  42384  fouriersw  42397  2exp340mod341  43745  8exp8mod9  43748  nfermltl8rev  43754  tgblthelfgott  43827  zlmodzxzequa  44449  zlmodzxzequap  44452
  Copyright terms: Public domain W3C validator