![]() |
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 478 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantll 476 |
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 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: mpteqb 5601 mpofun 5970 xpdom2 6824 addcmpblnq 7344 addpipqqslem 7346 addpipqqs 7347 addclnq 7352 addcomnqg 7358 addassnqg 7359 mulcomnqg 7360 mulassnqg 7361 distrnqg 7364 ltdcnq 7374 enq0ref 7410 addcmpblnq0 7420 addclnq0 7428 nqpnq0nq 7430 nqnq0a 7431 nqnq0m 7432 distrnq0 7436 mulcomnq0 7437 addassnq0lemcl 7438 genpdisj 7500 appdiv0nq 7541 addcomsrg 7732 mulcomsrg 7734 mulasssrg 7735 distrsrg 7736 addcnsr 7811 mulcnsr 7812 addcnsrec 7819 axaddcl 7841 axmulcl 7843 axaddcom 7847 add42 8096 muladd 8318 mulsub 8335 apreim 8537 divmuleqap 8650 ltmul12a 8793 lemul12b 8794 lemul12a 8795 qaddcl 9611 qmulcl 9613 iooshf 9926 fzass4 10035 elfzomelpfzo 10204 tanaddaplem 11717 opnneissb 13288 neitx 13401 txcnmpt 13406 txrest 13409 metcnp3 13644 cncfmet 13712 dveflem 13820 lgsdir2 14067 |
Copyright terms: Public domain | W3C validator |