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

Theorem mpanr1 702
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 469 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 700 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:  mpanr12  704  oacl  8530  omcl  8531  oaordi  8542  oawordri  8546  oaass  8557  oarec  8558  omordi  8562  omwordri  8568  odi  8575  omass  8576  oeoelem  8594  undom  9055  fimax2g  9285  fimin2g  9488  frr1  9750  axcnre  11155  divdiv23zi  11963  recp1lt1  12108  divgt0i  12118  divge0i  12119  ltreci  12120  lereci  12121  lt2msqi  12122  le2msqi  12123  msq11i  12124  ltdiv23i  12134  ltdivp1i  12136  zmin  12924  ge0gtmnf  13147  hashprg  14351  sqrt11i  15327  sqrtmuli  15328  sqrtmsq2i  15330  sqrtlei  15331  sqrtlti  15332  cos01gt0  16130  wspthsnwspthsnon  29150  vc2OLD  29799  vc0  29805  vcm  29807  nvpi  29898  nvge0  29904  ipval3  29940  ipidsq  29941  sspmval  29964  opsqrlem1  31371  opsqrlem6  31376  hstle  31461  hstrbi  31497  atordi  31615  finorwe  36201  poimirlem6  36432  poimirlem7  36433  poimirlem16  36442  poimirlem19  36445  poimirlem20  36446
  Copyright terms: Public domain W3C validator