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

Theorem anim12d 546
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
Hypotheses
Ref Expression
anim12d.1
anim12d.2
Assertion
Ref Expression
anim12d

Proof of Theorem anim12d
StepHypRef Expression
1 anim12d.1 . 2
2 anim12d.2 . 2
3 idd 21 . 2
41, 2, 3syl2and 469 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:  anim1d  547  anim2d  548  prth  554  im2anan9  808  anim12dan  810  3anim123d  1259  2euswap  2280  ssunsn2  3865  leltfintr  4458  ltfintr  4459  xp11  5056  2elresin  5194  fun  5236  dff13  5471  isotr  5495  enmap2lem4  6066  enmap1lem4  6072  nnltp1c  6262  nchoicelem17  6305  fnfrec  6320
  Copyright terms: Public domain W3C validator