![]() |
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 107 | . 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓) | |
2 | adantrd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | syl5 32 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem is referenced by: syldan 276 jaoa 673 prlem1 915 equveli 1684 elssabg 3949 suctr 4212 fvun1 5315 opabbrex 5628 poxp 5932 tposfo2 5964 1idprl 7052 1idpru 7053 uzind 8753 xrlttr 9160 fzen 9352 fz0fzelfz0 9429 zeqzmulgcd 10742 lcmgcdlem 10839 lcmdvds 10841 cncongr2 10866 exprmfct 10899 bj-om 11175 |
Copyright terms: Public domain | W3C validator |