![]() |
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 4145 suctr 4418 fvun1 5578 opabbrex 5913 poxp 6227 tposfo2 6262 1idprl 7577 1idpru 7578 uzind 9350 xrlttr 9779 fzen 10026 fz0fzelfz0 10110 fisumss 11381 fprodssdc 11579 zeqzmulgcd 11951 lcmgcdlem 12057 lcmdvds 12059 cncongr2 12084 exprmfct 12118 pceu 12275 infpnlem1 12337 ringadd2 13033 metrest 13666 bj-charfunbi 14212 bj-om 14338 |
Copyright terms: Public domain | W3C validator |