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 672 prlem1 914 equveli 1682 elssabg 3923 suctr 4176 fvun1 5260 opabbrex 5569 poxp 5873 tposfo2 5905 1idprl 6780 1idpru 6781 uzind 8458 xrlttr 8870 fzen 9062 fz0fzelfz0 9138 zeqzmulgcd 10362 lcmgcdlem 10459 lcmdvds 10461 cncongr2 10486 exprmfct 10519 bj-om 10732 |
Copyright terms: Public domain | W3C validator |