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 474 . 2 (𝜑𝜓)
4 mp4an.3 . . 3 𝜒
5 mp4an.4 . . 3 𝜃
64, 5pm3.2i 474 . 2 (𝜒𝜃)
7 mp4an.5 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
83, 6, 7mp2an 691 1 𝜏
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  noinfep  9111  1lt2nq  10388  m1p1sr  10507  m1m1sr  10508  axi2m1  10574  mul4i  10830  add4i  10857  add42i  10858  addsub4i  10975  muladdi  11084  lt2addi  11195  le2addi  11196  mulne0i  11276  divne0i  11381  divmuldivi  11393  divadddivi  11395  divdivdivi  11396  subreci  11463  8th4div3  11849  xrsup0  12708  fldiv4p1lem1div2  13204  sqrt2gt1lt2  14630  3dvds2dec  15678  flodddiv4  15758  nprmi  16027  mod2xnegi  16401  catcfuccl  17365  catcxpccl  17453  iccpnfhmeo  23554  xrhmeo  23555  cnheiborlem  23563  pcoval1  23622  pcoval2  23625  pcoass  23633  lhop1lem  24620  efcvx  25048  cos0pilt1  25128  dvrelog  25232  dvlog  25246  dvlog2  25248  dvsqrt  25335  dvcnsqrt  25337  cxpcn3  25341  ang180lem1  25399  dvatan  25525  log2cnv  25534  log2tlbnd  25535  log2ub  25539  harmonicbnd3  25597  ppiub  25792  bposlem8  25879  bposlem9  25880  lgsdir2lem1  25913  m1lgs  25976  2lgslem4  25994  2sqlem11  26017  2sqreultlem  26035  2sqreunnltlem  26038  chebbnd1  26060  usgrexmplef  27053  siilem1  28638  hvadd4i  28845  his35i  28876  bdophsi  29883  bdopcoi  29885  mdcompli  30216  dmdcompli  30217  cshw1s2  30664  xrge00  30724  sqsscirc1  31265  raddcn  31286  xrge0iifcnv  31290  xrge0iifiso  31292  xrge0iifhom  31294  esumcvgsum  31461  dstfrvclim1  31849  signsply0  31935  cvmlift2lem6  32669  cvmlift2lem12  32675  iccioo01  34742  poimirlem9  35065  poimirlem15  35071  sqdeccom12  39480  lhe4.4ex1a  41030  dvcosre  42551  wallispi  42709  fourierdlem57  42802  fourierdlem58  42803  fourierdlem112  42857  fouriersw  42870  2exp340mod341  44248  8exp8mod9  44251  nfermltl8rev  44257  tgblthelfgott  44330  zlmodzxzequa  44902  zlmodzxzequap  44905
  Copyright terms: Public domain W3C validator