New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  anidms GIF version

Theorem anidms 626
 Description: Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.)
Hypothesis
Ref Expression
anidms.1 ((φ φ) → ψ)
Assertion
Ref Expression
anidms (φψ)

Proof of Theorem anidms
StepHypRef Expression
1 anidms.1 . . 3 ((φ φ) → ψ)
21ex 423 . 2 (φ → (φψ))
32pm2.43i 43 1 (φψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  sylancb  646  sylancbr  647  compleq  3243  dedth2v  3707  dedth3v  3708  dedth4v  3709  intsng  3961  complexg  4099  pw1exg  4302  ltfinirr  4457  lefinrflx  4467  0ceven  4505  evennn  4506  oddnn  4507  sucoddeven  4511  evenodddisj  4516  eventfin  4517  oddtfin  4518  nnpweq  4523  sfindbl  4530  sfintfin  4532  xpid11  4926  dfxp2  5113  brtxp  5783  elfix  5787  lecidg  6196  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  nnc3p1n3p2  6280  nchoicelem1  6289  nchoicelem2  6290
 Copyright terms: Public domain W3C validator