![]() |
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 967 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜓) |
3 | 3anim123i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 3 | 3ad2ant2 968 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜃) |
5 | 3anim123i.3 | . . 3 ⊢ (𝜏 → 𝜂) | |
6 | 5 | 3ad2ant3 969 | . 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) |
7 | 2, 4, 6 | 3jca 1126 | 1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 927 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: 3anim1i 1132 3anim2i 1133 3anim3i 1134 syl3an 1223 syl3anl 1232 spc3egv 2724 spc3gv 2725 eloprabga 5773 le2tri3i 7690 fzmmmeqm 9621 elfz1b 9653 elfz0fzfz0 9686 elfzmlbp 9692 elfzo1 9750 flltdivnn0lt 9860 modmulconst 11270 nndvdslegcd 11399 |
Copyright terms: Public domain | W3C validator |