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

Theorem anabsi7 669
Description: Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
Hypothesis
Ref Expression
anabsi7.1 (𝜓 → ((𝜑𝜓) → 𝜒))
Assertion
Ref Expression
anabsi7 ((𝜑𝜓) → 𝜒)

Proof of Theorem anabsi7
StepHypRef Expression
1 anabsi7.1 . . 3 (𝜓 → ((𝜑𝜓) → 𝜒))
21anabsi6 668 . 2 ((𝜓𝜑) → 𝜒)
32ancoms 459 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  syldbl2  839  nelrdva  3697  elunii  4906  ordelord  6375  fvelrn  7063  onsucuni2  7805  fnfi  9164  prnmax  10972  relexpindlem  14992  opreu2reuALT  31580  ralssiun  36092  monotoddzz  41453  oddcomabszz  41454  flcidc  41687  fmul01  44069  fprodcnlem  44088  stoweidlem4  44493  stoweidlem20  44509  stoweidlem22  44511  stoweidlem27  44516  stoweidlem30  44519  stoweidlem51  44540  stoweidlem59  44548  fourierdlem21  44617  fourierdlem89  44684  fourierdlem90  44685  fourierdlem91  44686  fourierdlem104  44699
  Copyright terms: Public domain W3C validator