![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad2ant2rl | Unicode version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.) |
Ref | Expression |
---|---|
ad2ant2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ad2ant2rl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantrl 462 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantlr 461 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: fvtp1g 5505 fcof1o 5568 infnfi 6611 addcomnqg 6940 addassnqg 6941 nqtri3or 6955 ltexnqq 6967 nqnq0pi 6997 nqpnq0nq 7012 nqnq0a 7013 addassnq0lemcl 7020 ltaddpr 7156 ltexprlemloc 7166 addcanprlemu 7174 recexprlem1ssu 7193 aptiprleml 7198 mulcomsrg 7303 mulasssrg 7304 distrsrg 7305 aptisr 7324 mulcnsr 7372 cnegex 7660 muladd 7862 lemul12b 8322 qaddcl 9120 iooshf 9370 elfzomelpfzo 9642 expnegzap 9989 setscom 11534 |
Copyright terms: Public domain | W3C validator |