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

Theorem mpanl1 699
 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 527 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 583 1 ((𝜓𝜒) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  mpanl12  701  frc  5508  oeoelem  8220  ercnv  8306  frfi  8760  fin23lem23  9746  divdiv23zi  11391  recp1lt1  11536  divgt0i  11546  divge0i  11547  ltreci  11548  lereci  11549  lt2msqi  11550  le2msqi  11551  msq11i  11552  ltdiv23i  11562  fnn0ind  12078  elfzp1b  12988  elfzm1b  12989  sqrt11i  14744  sqrtmuli  14745  sqrtmsq2i  14747  sqrtlei  14748  sqrtlti  14749  fsum  15077  fprod  15295  blometi  28592  spansnm0i  29439  lnopli  29757  lnfnli  29829  opsqrlem1  29929  opsqrlem6  29934  mdslmd3i  30121  atordi  30173  mdsymlem1  30192  gsummpt2co  30721  finxpreclem4  34759  ptrecube  35005  fdc  35131  prter3  36126
 Copyright terms: Public domain W3C validator