New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  anim12d GIF 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-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:  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