![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad2ant2l | Unicode version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
ad2ant2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ad2ant2l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantrl 463 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantll 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 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: mpteqb 5408 mpt2fun 5763 xpdom2 6603 addcmpblnq 6989 addpipqqslem 6991 addpipqqs 6992 addclnq 6997 addcomnqg 7003 addassnqg 7004 mulcomnqg 7005 mulassnqg 7006 distrnqg 7009 ltdcnq 7019 enq0ref 7055 addcmpblnq0 7065 addclnq0 7073 nqpnq0nq 7075 nqnq0a 7076 nqnq0m 7077 distrnq0 7081 mulcomnq0 7082 addassnq0lemcl 7083 genpdisj 7145 appdiv0nq 7186 addcomsrg 7364 mulcomsrg 7366 mulasssrg 7367 distrsrg 7368 addcnsr 7434 mulcnsr 7435 addcnsrec 7442 axaddcl 7464 axmulcl 7466 axaddcom 7468 add42 7707 muladd 7925 mulsub 7942 apreim 8143 divmuleqap 8247 ltmul12a 8384 lemul12b 8385 lemul12a 8386 qaddcl 9183 qmulcl 9185 iooshf 9433 fzass4 9539 elfzomelpfzo 9705 tanaddaplem 11092 opnneissb 11918 |
Copyright terms: Public domain | W3C validator |