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

Theorem anabsi7 856
 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 855 . 2 ((𝜓𝜑) → 𝜒)
32ancoms 468 1 ((𝜑𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  syl2an23an  1379  nelrdva  3384  elunii  4377  ordelord  5662  fvelrn  6260  onsucuni2  6926  fnfi  8123  prnmax  9696  monotoddzz  36526  oddcomabszz  36527  flcidc  36763  syldbl2  37490  fmul01  38647  fprodcnlem  38666  stoweidlem4  38897  stoweidlem20  38913  stoweidlem22  38915  stoweidlem27  38920  stoweidlem30  38923  stoweidlem51  38944  stoweidlem59  38952  fourierdlem21  39021  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem104  39103
 Copyright terms: Public domain W3C validator