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

Theorem mpanl1 716
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 564 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 488 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  mpanl12  718  frc  5078  oeoelem  7675  ercnv  7760  frfi  8202  fin23lem23  9145  divdiv23zi  10775  recp1lt1  10918  divgt0i  10929  divge0i  10930  ltreci  10931  lereci  10932  lt2msqi  10933  le2msqi  10934  msq11i  10935  ltdiv23i  10945  fnn0ind  11473  elfzp1b  12413  elfzm1b  12414  sqrt11i  14118  sqrtmuli  14119  sqrtmsq2i  14121  sqrtlei  14122  sqrtlti  14123  fsum  14445  fprod  14665  blometi  27642  spansnm0i  28493  lnopli  28811  lnfnli  28883  opsqrlem1  28983  opsqrlem6  28988  mdslmd3i  29175  atordi  29227  mdsymlem1  29246  gsummpt2co  29765  finxpreclem4  33211  ptrecube  33389  fdc  33521  prter3  33993
  Copyright terms: Public domain W3C validator