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 447 | . 2 |
3 | 2 | adantll 445 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: mpteqb 5261 mpt2fun 5603 xpdom2 6305 addcmpblnq 6465 addpipqqslem 6467 addpipqqs 6468 addclnq 6473 addcomnqg 6479 addassnqg 6480 mulcomnqg 6481 mulassnqg 6482 distrnqg 6485 ltdcnq 6495 enq0ref 6531 addcmpblnq0 6541 addclnq0 6549 nqpnq0nq 6551 nqnq0a 6552 nqnq0m 6553 distrnq0 6557 mulcomnq0 6558 addassnq0lemcl 6559 genpdisj 6621 appdiv0nq 6662 addcomsrg 6840 mulcomsrg 6842 mulasssrg 6843 distrsrg 6844 addcnsr 6910 mulcnsr 6911 addcnsrec 6918 axaddcl 6940 axmulcl 6942 axaddcom 6944 add42 7173 muladd 7381 mulsub 7398 apreim 7594 divmuleqap 7693 ltmul12a 7826 lemul12b 7827 lemul12a 7828 qaddcl 8570 qmulcl 8572 iooshf 8821 fzass4 8925 elfzomelpfzo 9087 |
Copyright terms: Public domain | W3C validator |