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

Theorem anim2i 552
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
anim1i.1 (φψ)
Assertion
Ref Expression
anim2i ((χ φ) → (χ ψ))

Proof of Theorem anim2i
StepHypRef Expression
1 id 19 . 2 (χχ)
2 anim1i.1 . 2 (φψ)
31, 2anim12i 549 1 ((χ φ) → (χ ψ))
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
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 177  df-an 360
This theorem is referenced by:  sylanl2  632  sylanr2  634  andi  837  sbimi  1652  19.41  1879  ax12olem2  1928  exdistrf  1971  equs45f  1989  eupickb  2269  2eu1  2284  darii  2303  festino  2309  baroco  2310  r19.27av  2752  rspc2ev  2963  reu3  3026  difrab  3529  sfinltfin  4535  vfinspnn  4541  vinf  4555  fof  5269  fv3  5341  fvelimab  5370  fvopab4t  5385  dff2  5419  dffo5  5424  dff1o6  5475  oprabid  5550  ssoprab2i  5580  ndmovass  5618  ndmovdistr  5619  oqelins4  5794
  Copyright terms: Public domain W3C validator