![]() |
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 1020 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓) |
3 | 3anim123i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 3 | 3ad2ant2 1021 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃) |
5 | 3anim123i.3 | . . 3 ⊢ (𝜏 → 𝜂) | |
6 | 5 | 3ad2ant3 1022 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) |
7 | 2, 4, 6 | 3jca 1179 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 980 |
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 df-3an 982 |
This theorem is referenced by: 3anim1i 1187 3anim2i 1188 3anim3i 1189 syl3an 1291 syl3anl 1300 spc3egv 2844 spc3gv 2845 eloprabga 5979 le2tri3i 8091 fzmmmeqm 10083 elfz1b 10115 elfz0fzfz0 10151 elfzmlbp 10157 elfzo1 10215 flltdivnn0lt 10330 modmulconst 11857 nndvdslegcd 11993 lgsmulsqcoprm 14884 |
Copyright terms: Public domain | W3C validator |