| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > anim12dan | GIF version | ||
| Description: Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.) |
| Ref | Expression |
|---|---|
| anim12dan.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| anim12dan.2 | ⊢ ((𝜑 ∧ 𝜃) → 𝜏) |
| Ref | Expression |
|---|---|
| anim12dan | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | anim12dan.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
| 2 | 1 | ex 115 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
| 3 | anim12dan.2 | . . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜏) | |
| 4 | 3 | ex 115 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜏)) |
| 5 | 2, 4 | anim12d 335 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
| 6 | 5 | imp 124 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 |
| This theorem is referenced by: xpexr2m 5178 isocnv 5952 f1oiso 5967 f1oiso2 5968 f1o2ndf1 6393 xpf1o 7030 pc11 12906 imasaddfnlemg 13399 imasaddflemg 13401 mhmpropd 13551 ghmsub 13840 invrpropdg 14166 znidom 14674 tgclb 14792 innei 14890 txcn 15002 plymullem1 15475 lgsdir2 15765 |
| Copyright terms: Public domain | W3C validator |