![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adantrd | Unicode 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: ![]() ![]() |
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 720 prlem1 973 equveli 1759 elssabg 4150 suctr 4423 fvun1 5584 opabbrex 5921 poxp 6235 tposfo2 6270 1idprl 7591 1idpru 7592 uzind 9366 xrlttr 9797 fzen 10045 fz0fzelfz0 10129 fisumss 11402 fprodssdc 11600 zeqzmulgcd 11973 lcmgcdlem 12079 lcmdvds 12081 cncongr2 12106 exprmfct 12140 pceu 12297 infpnlem1 12359 ringadd2 13215 metrest 14045 bj-charfunbi 14602 bj-om 14728 |
Copyright terms: Public domain | W3C validator |