![]() |
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 109 | . 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓) | |
2 | adantrd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | syl5 32 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem is referenced by: syldan 282 jaoa 721 prlem1 974 equveli 1769 elssabg 4160 suctr 4433 fvun1 5595 opabbrex 5932 poxp 6246 tposfo2 6281 1idprl 7602 1idpru 7603 uzind 9377 xrlttr 9808 fzen 10056 fz0fzelfz0 10140 fisumss 11413 fprodssdc 11611 zeqzmulgcd 11984 lcmgcdlem 12090 lcmdvds 12092 cncongr2 12117 exprmfct 12151 pceu 12308 infpnlem1 12370 ringadd2 13264 metrest 14233 bj-charfunbi 14790 bj-om 14916 |
Copyright terms: Public domain | W3C validator |