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

Theorem mpanl1 711
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpanl1.1 𝜑
mpanl1.2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
mpanl1 ((𝜓𝜒) → 𝜃)

Proof of Theorem mpanl1
StepHypRef Expression
1 mpanl1.1 . . 3 𝜑
21jctl 561 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 486 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  mpanl12  713  frc  4990  oeoelem  7538  ercnv  7623  frfi  8063  fin23lem23  9004  divdiv23zi  10623  recp1lt1  10766  divgt0i  10777  divge0i  10778  ltreci  10779  lereci  10780  lt2msqi  10781  le2msqi  10782  msq11i  10783  ltdiv23i  10793  fnn0ind  11304  elfzp1b  12237  elfzm1b  12238  sqrt11i  13914  sqrtmuli  13915  sqrtmsq2i  13917  sqrtlei  13918  sqrtlti  13919  fsum  14240  fprod  14452  blometi  26844  spansnm0i  27695  lnopli  28013  lnfnli  28085  opsqrlem1  28185  opsqrlem6  28190  mdslmd3i  28377  atordi  28429  mdsymlem1  28448  gsummpt2co  28913  finxpreclem4  32206  ptrecube  32378  fdc  32510  prter3  32984
  Copyright terms: Public domain W3C validator