![]() |
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 4149 suctr 4422 fvun1 5583 opabbrex 5919 poxp 6233 tposfo2 6268 1idprl 7589 1idpru 7590 uzind 9364 xrlttr 9795 fzen 10043 fz0fzelfz0 10127 fisumss 11400 fprodssdc 11598 zeqzmulgcd 11971 lcmgcdlem 12077 lcmdvds 12079 cncongr2 12104 exprmfct 12138 pceu 12295 infpnlem1 12357 ringadd2 13210 metrest 14009 bj-charfunbi 14566 bj-om 14692 |
Copyright terms: Public domain | W3C validator |