Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ad2ant2lr | Unicode version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.) |
Ref | Expression |
---|---|
ad2ant2.1 |
Ref | Expression |
---|---|
ad2ant2lr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 | . . 3 | |
2 | 1 | adantrr 476 | . 2 |
3 | 2 | adantll 473 | 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 5586 fiunsnnn 6859 addcomnqg 7343 addassnqg 7344 nqtri3or 7358 lt2addnq 7366 lt2mulnq 7367 enq0ref 7395 enq0tr 7396 nqnq0pi 7400 nqpnq0nq 7415 nqnq0a 7416 distrnq0 7421 addassnq0lemcl 7423 ltsrprg 7709 mulcomsrg 7719 mulasssrg 7720 distrsrg 7721 aptisr 7741 mulcnsr 7797 cnegex 8097 sub4 8164 muladd 8303 ltleadd 8365 divdivdivap 8630 divadddivap 8644 ltmul12a 8776 fzrev 10040 facndiv 10673 cncongr1 12057 blbas 13227 cncfmet 13373 ptolemy 13539 |
Copyright terms: Public domain | W3C validator |