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

Theorem mpanr1 703
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 467 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 701 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  mpanr12  705  oacl  8574  omcl  8575  oaordi  8585  oawordri  8589  oaass  8600  oarec  8601  omordi  8605  omwordri  8611  odi  8618  omass  8619  oeoelem  8637  undom  9100  fimax2g  9323  fimin2g  9538  frr1  9800  axcnre  11205  divdiv23zi  12021  recp1lt1  12167  divgt0i  12177  divge0i  12178  ltreci  12179  lereci  12180  lt2msqi  12181  le2msqi  12182  msq11i  12183  ltdiv23i  12193  ltdivp1i  12195  zmin  12987  ge0gtmnf  13215  hashprg  14435  sqrt11i  15424  sqrtmuli  15425  sqrtmsq2i  15427  sqrtlei  15428  sqrtlti  15429  cos01gt0  16228  wspthsnwspthsnon  29937  vc2OLD  30588  vc0  30594  vcm  30596  nvpi  30687  nvge0  30693  ipval3  30729  ipidsq  30730  sspmval  30753  opsqrlem1  32160  opsqrlem6  32165  hstle  32250  hstrbi  32286  atordi  32404  weiunlem2  36465  finorwe  37384  poimirlem6  37634  poimirlem7  37635  poimirlem16  37644  poimirlem19  37647  poimirlem20  37648
  Copyright terms: Public domain W3C validator