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

Theorem mpanr1 715
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
mpanr1.1 𝜓
mpanr1.2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
mpanr1 ((𝜑𝜒) → 𝜃)

Proof of Theorem mpanr1
StepHypRef Expression
1 mpanr1.1 . 2 𝜓
2 mpanr1.2 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32anassrs 678 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 713 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 196  df-an 385
This theorem is referenced by:  mpanr12  717  oacl  7502  omcl  7503  oaordi  7513  oawordri  7517  oaass  7528  oarec  7529  omordi  7533  omwordri  7539  odi  7546  omass  7547  oeoelem  7565  fimax2g  8091  fimin2g  8286  axcnre  9864  divdiv23zi  10657  recp1lt1  10800  divgt0i  10811  divge0i  10812  ltreci  10813  lereci  10814  lt2msqi  10815  le2msqi  10816  msq11i  10817  ltdiv23i  10827  ltdivp1i  10829  zmin  11660  ge0gtmnf  11877  hashprg  13043  hashprgOLD  13044  sqrt11i  13972  sqrtmuli  13973  sqrtmsq2i  13975  sqrtlei  13976  sqrtlti  13977  cos01gt0  14760  0wlk  26075  0trl  26076  0pth  26100  0spth  26101  0crct  26154  0cycl  26155  0clwlk  26293  vc2OLD  26807  vc0  26813  vcm  26815  nvpi  26906  nvge0  26912  ipval3  26948  ipidsq  26949  sspmval  26972  opsqrlem1  28383  opsqrlem6  28388  hstle  28473  hstrbi  28509  atordi  28627  poimirlem6  32585  poimirlem7  32586  poimirlem16  32595  poimirlem19  32598  poimirlem20  32599
  Copyright terms: Public domain W3C validator