![]() |
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 975 equveli 1770 elssabg 4163 suctr 4436 fvun1 5598 opabbrex 5935 poxp 6251 tposfo2 6286 1idprl 7607 1idpru 7608 uzind 9382 xrlttr 9813 fzen 10061 fz0fzelfz0 10145 fisumss 11418 fprodssdc 11616 zeqzmulgcd 11989 lcmgcdlem 12095 lcmdvds 12097 cncongr2 12122 exprmfct 12156 pceu 12313 infpnlem1 12375 isghm 13143 ringadd2 13342 metrest 14403 bj-charfunbi 14960 bj-om 15086 |
Copyright terms: Public domain | W3C validator |