![]() |
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 639 prlem1 879 equveli 1639 elssabg 3893 suctr 4124 fvun1 5182 opabbrex 5491 poxp 5794 tposfo2 5823 1idprl 6566 1idpru 6567 uzind 8125 xrlttr 8486 fzen 8677 fz0fzelfz0 8754 bj-om 9396 |
Copyright terms: Public domain | W3C validator |