Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > adantrd | GIF version |
Description: Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.) |
Ref | Expression |
---|---|
adantrd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
adantrd | ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 102 | . 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓) | |
2 | adantrd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | syl5 28 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem is referenced by: syldan 266 jaoa 640 prlem1 880 equveli 1642 elssabg 3902 suctr 4158 fvun1 5239 opabbrex 5549 poxp 5853 tposfo2 5882 1idprl 6688 1idpru 6689 uzind 8349 xrlttr 8716 fzen 8907 fz0fzelfz0 8984 bj-om 10061 |
Copyright terms: Public domain | W3C validator |