Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3anim123i | GIF version |
Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3anim123i.1 | ⊢ (𝜑 → 𝜓) |
3anim123i.2 | ⊢ (𝜒 → 𝜃) |
3anim123i.3 | ⊢ (𝜏 → 𝜂) |
Ref | Expression |
---|---|
3anim123i | ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anim123i.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | 3ad2ant1 959 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓) |
3 | 3anim123i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 3 | 3ad2ant2 960 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃) |
5 | 3anim123i.3 | . . 3 ⊢ (𝜏 → 𝜂) | |
6 | 5 | 3ad2ant3 961 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) |
7 | 2, 4, 6 | 3jca 1118 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 919 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 921 |
This theorem is referenced by: 3anim1i 1124 3anim2i 1125 3anim3i 1126 syl3an 1211 syl3anl 1220 spc3egv 2689 spc3gv 2690 eloprabga 5611 le2tri3i 7219 fzmmmeqm 9076 elfz1b 9107 elfz0fzfz0 9137 elfzmlbp 9143 elfzo1 9199 flltdivnn0lt 9306 modmulconst 10227 nndvdslegcd 10357 |
Copyright terms: Public domain | W3C validator |