New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > anim12d | GIF version |
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |
Ref | Expression |
---|---|
anim12d.1 | ⊢ (φ → (ψ → χ)) |
anim12d.2 | ⊢ (φ → (θ → τ)) |
Ref | Expression |
---|---|
anim12d | ⊢ (φ → ((ψ ∧ θ) → (χ ∧ τ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim12d.1 | . 2 ⊢ (φ → (ψ → χ)) | |
2 | anim12d.2 | . 2 ⊢ (φ → (θ → τ)) | |
3 | idd 21 | . 2 ⊢ (φ → ((χ ∧ τ) → (χ ∧ τ))) | |
4 | 1, 2, 3 | syl2and 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 |