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

Theorem mpanr1 700
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 468 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 698 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  mpanr12  702  oacl  8365  omcl  8366  oaordi  8377  oawordri  8381  oaass  8392  oarec  8393  omordi  8397  omwordri  8403  odi  8410  omass  8411  oeoelem  8429  undom  8846  fimax2g  9060  fimin2g  9256  frr1  9517  axcnre  10920  divdiv23zi  11728  recp1lt1  11873  divgt0i  11883  divge0i  11884  ltreci  11885  lereci  11886  lt2msqi  11887  le2msqi  11888  msq11i  11889  ltdiv23i  11899  ltdivp1i  11901  zmin  12684  ge0gtmnf  12906  hashprg  14110  sqrt11i  15096  sqrtmuli  15097  sqrtmsq2i  15099  sqrtlei  15100  sqrtlti  15101  cos01gt0  15900  wspthsnwspthsnon  28281  vc2OLD  28930  vc0  28936  vcm  28938  nvpi  29029  nvge0  29035  ipval3  29071  ipidsq  29072  sspmval  29095  opsqrlem1  30502  opsqrlem6  30507  hstle  30592  hstrbi  30628  atordi  30746  finorwe  35553  poimirlem6  35783  poimirlem7  35784  poimirlem16  35793  poimirlem19  35796  poimirlem20  35797
  Copyright terms: Public domain W3C validator