Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anim1d | GIF version |
Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
anim1d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
anim1d | ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | idd 21 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
3 | 1, 2 | anim12d 333 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm3.45 587 exdistrfor 1787 mopick2 2096 ssrexf 3199 ssrexv 3202 ssdif 3252 ssrin 3342 reupick 3401 disjss1 3959 copsexg 4216 po3nr 4282 coss2 4754 fununi 5250 fiintim 6885 recexprlemlol 7558 recexprlemupu 7560 icoshft 9917 2ffzeq 10066 qbtwnxr 10183 ico0 10187 r19.2uz 10921 bezoutlemzz 11920 bezoutlemaz 11921 neiss 12697 uptx 12821 txcn 12822 bj-charfundcALT 13532 |
Copyright terms: Public domain | W3C validator |