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

Theorem mpanl1 688
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 516 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 572 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387
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 199  df-an 388
This theorem is referenced by:  mpanl12  690  frc  5369  oeoelem  8023  ercnv  8108  frfi  8556  fin23lem23  9544  divdiv23zi  11192  recp1lt1  11337  divgt0i  11347  divge0i  11348  ltreci  11349  lereci  11350  lt2msqi  11351  le2msqi  11352  msq11i  11353  ltdiv23i  11363  fnn0ind  11892  elfzp1b  12798  elfzm1b  12799  sqrt11i  14603  sqrtmuli  14604  sqrtmsq2i  14606  sqrtlei  14607  sqrtlti  14608  fsum  14935  fprod  15153  blometi  28372  spansnm0i  29223  lnopli  29541  lnfnli  29613  opsqrlem1  29713  opsqrlem6  29718  mdslmd3i  29905  atordi  29957  mdsymlem1  29976  gsummpt2co  30555  finxpreclem4  34153  ptrecube  34370  fdc  34499  prter3  35500
  Copyright terms: Public domain W3C validator