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 469 | . 2 |
3 | 2 | adantll 467 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: mpteqb 5479 mpofun 5841 xpdom2 6693 addcmpblnq 7143 addpipqqslem 7145 addpipqqs 7146 addclnq 7151 addcomnqg 7157 addassnqg 7158 mulcomnqg 7159 mulassnqg 7160 distrnqg 7163 ltdcnq 7173 enq0ref 7209 addcmpblnq0 7219 addclnq0 7227 nqpnq0nq 7229 nqnq0a 7230 nqnq0m 7231 distrnq0 7235 mulcomnq0 7236 addassnq0lemcl 7237 genpdisj 7299 appdiv0nq 7340 addcomsrg 7531 mulcomsrg 7533 mulasssrg 7534 distrsrg 7535 addcnsr 7610 mulcnsr 7611 addcnsrec 7618 axaddcl 7640 axmulcl 7642 axaddcom 7646 add42 7892 muladd 8114 mulsub 8131 apreim 8333 divmuleqap 8445 ltmul12a 8586 lemul12b 8587 lemul12a 8588 qaddcl 9395 qmulcl 9397 iooshf 9703 fzass4 9810 elfzomelpfzo 9976 tanaddaplem 11372 opnneissb 12251 neitx 12364 txcnmpt 12369 txrest 12372 metcnp3 12607 cncfmet 12675 dveflem 12782 |
Copyright terms: Public domain | W3C validator |