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

Theorem mpanl1 700
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 523 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 580 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  mpanl12  702  frc  5648  oeoelem  8636  ercnv  8766  frfi  9321  fin23lem23  10366  divdiv23zi  12020  recp1lt1  12166  divgt0i  12176  divge0i  12177  ltreci  12178  lereci  12179  lt2msqi  12180  le2msqi  12181  msq11i  12182  ltdiv23i  12192  fnn0ind  12717  elfzp1b  13641  elfzm1b  13642  sqrt11i  15423  sqrtmuli  15424  sqrtmsq2i  15426  sqrtlei  15427  sqrtlti  15428  fsum  15756  fprod  15977  blometi  30822  spansnm0i  31669  lnopli  31987  lnfnli  32059  opsqrlem1  32159  opsqrlem6  32164  mdslmd3i  32351  atordi  32403  mdsymlem1  32422  gsummpt2co  33051  finxpreclem4  37395  ptrecube  37627  fdc  37752  prter3  38883
  Copyright terms: Public domain W3C validator