![]() |
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 467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantlr 466 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: fvtp1g 5582 fcof1o 5644 infnfi 6742 addcomnqg 7134 addassnqg 7135 nqtri3or 7149 ltexnqq 7161 nqnq0pi 7191 nqpnq0nq 7206 nqnq0a 7207 addassnq0lemcl 7214 ltaddpr 7350 ltexprlemloc 7360 addcanprlemu 7368 recexprlem1ssu 7387 aptiprleml 7392 mulcomsrg 7497 mulasssrg 7498 distrsrg 7499 aptisr 7518 mulcnsr 7567 cnegex 7860 muladd 8062 lemul12b 8526 qaddcl 9326 iooshf 9625 elfzomelpfzo 9898 expnegzap 10217 setscom 11839 cnpnei 12227 |
Copyright terms: Public domain | W3C validator |