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

Theorem mpanl1 680
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 513 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 569 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 197  df-an 383
This theorem is referenced by:  mpanl12  682  frc  5215  oeoelem  7832  ercnv  7917  frfi  8361  fin23lem23  9350  divdiv23zi  10980  recp1lt1  11123  divgt0i  11134  divge0i  11135  ltreci  11136  lereci  11137  lt2msqi  11138  le2msqi  11139  msq11i  11140  ltdiv23i  11150  fnn0ind  11678  elfzp1b  12624  elfzm1b  12625  sqrt11i  14332  sqrtmuli  14333  sqrtmsq2i  14335  sqrtlei  14336  sqrtlti  14337  fsum  14659  fprod  14878  blometi  27998  spansnm0i  28849  lnopli  29167  lnfnli  29239  opsqrlem1  29339  opsqrlem6  29344  mdslmd3i  29531  atordi  29583  mdsymlem1  29602  gsummpt2co  30120  finxpreclem4  33568  ptrecube  33742  fdc  33873  prter3  34690
  Copyright terms: Public domain W3C validator