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

Theorem mpanl1 697
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 579 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 206  df-an 396
This theorem is referenced by:  mpanl12  699  frc  5633  oeoelem  8594  ercnv  8721  frfi  9285  fin23lem23  10318  divdiv23zi  11965  recp1lt1  12110  divgt0i  12120  divge0i  12121  ltreci  12122  lereci  12123  lt2msqi  12124  le2msqi  12125  msq11i  12126  ltdiv23i  12136  fnn0ind  12659  elfzp1b  13576  elfzm1b  13577  sqrt11i  15329  sqrtmuli  15330  sqrtmsq2i  15332  sqrtlei  15333  sqrtlti  15334  fsum  15664  fprod  15883  blometi  30528  spansnm0i  31375  lnopli  31693  lnfnli  31765  opsqrlem1  31865  opsqrlem6  31870  mdslmd3i  32057  atordi  32109  mdsymlem1  32128  gsummpt2co  32671  finxpreclem4  36766  ptrecube  36982  fdc  37107  prter3  38246
  Copyright terms: Public domain W3C validator