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

Theorem mp4an 692
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 472 . 2 (𝜑𝜓)
4 mp4an.3 . . 3 𝜒
5 mp4an.4 . . 3 𝜃
64, 5pm3.2i 472 . 2 (𝜒𝜃)
7 mp4an.5 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
83, 6, 7mp2an 691 1 𝜏
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  noinfep  9601  1lt2nq  10914  m1p1sr  11033  m1m1sr  11034  axi2m1  11100  mul4i  11357  add4i  11384  add42i  11385  addsub4i  11502  muladdi  11611  lt2addi  11722  le2addi  11723  mulne0i  11803  divne0i  11908  divmuldivi  11920  divadddivi  11922  divdivdivi  11923  subreci  11990  8th4div3  12378  xrsup0  13248  fldiv4p1lem1div2  13746  sqrt2gt1lt2  15165  3dvds2dec  16220  flodddiv4  16300  nprmi  16570  mod2xnegi  16948  catcfuccl  18010  catcfucclOLD  18011  catcxpccl  18100  catcxpcclOLD  18101  iccpnfhmeo  24324  xrhmeo  24325  cnheiborlem  24333  pcoval1  24392  pcoval2  24395  pcoass  24403  lhop1lem  25393  efcvx  25824  cos0pilt1  25904  dvrelog  26008  dvlog  26022  dvlog2  26024  dvsqrt  26111  dvcnsqrt  26113  cxpcn3  26117  ang180lem1  26175  dvatan  26301  log2cnv  26310  log2tlbnd  26311  log2ub  26315  harmonicbnd3  26373  ppiub  26568  bposlem8  26655  bposlem9  26656  lgsdir2lem1  26689  m1lgs  26752  2lgslem4  26770  2sqlem11  26793  2sqreultlem  26811  2sqreunnltlem  26814  chebbnd1  26836  0slt1s  27190  mulsproplem6  27406  mulsproplem7  27407  mulsproplem8  27408  mulsproplem9  27409  usgrexmplef  28249  siilem1  29835  hvadd4i  30042  his35i  30073  bdophsi  31080  bdopcoi  31082  mdcompli  31413  dmdcompli  31414  cshw1s2  31863  xrge00  31926  sqsscirc1  32546  raddcn  32567  xrge0iifcnv  32571  xrge0iifiso  32573  xrge0iifhom  32575  esumcvgsum  32744  dstfrvclim1  33134  signsply0  33220  cvmlift2lem6  33959  cvmlift2lem12  33965  iccioo01  35844  poimirlem9  36133  poimirlem15  36139  sqdeccom12  40846  lhe4.4ex1a  42697  dvcosre  44239  wallispi  44397  fourierdlem57  44490  fourierdlem58  44491  fourierdlem112  44545  fouriersw  44558  2exp340mod341  46011  8exp8mod9  46014  nfermltl8rev  46020  tgblthelfgott  46093  zlmodzxzequa  46663  zlmodzxzequap  46666  sepfsepc  47046
  Copyright terms: Public domain W3C validator