![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad3antlr | Unicode version |
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ad3antlr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ad2antlr 489 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantr 276 |
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: ad4antlr 495 nntr2 6503 phpm 6864 phplem4on 6866 fidifsnen 6869 fisbth 6882 fin0 6884 fin0or 6885 fiintim 6927 fisseneq 6930 djudom 7091 difinfsnlem 7097 nnnninfeq 7125 nnnninfeq2 7126 enomnilem 7135 enmkvlem 7158 enwomnilem 7166 exmidapne 7258 prmuloc 7564 cauappcvgprlemopl 7644 cauappcvgprlemdisj 7649 cauappcvgprlemladdfl 7653 caucvgprlemopl 7667 axcaucvglemcau 7896 xnn0letri 9801 xaddf 9842 xleaddadd 9885 ssfzo12bi 10222 rebtwn2zlemstep 10250 btwnzge0 10297 addmodlteq 10395 frecuzrdgg 10413 qsqeqor 10627 apexp1 10693 hashxp 10801 cjap 10910 caucvgre 10985 minmax 11233 xrminmax 11268 sumeq2 11362 fsumconst 11457 ntrivcvgap 11551 prodeq2 11560 p1modz1 11796 bezoutlemmain 11993 dfgcd2 12009 uzwodc 12032 lcmgcdlem 12071 mulgval 12940 cnpnei 13612 cnntr 13618 txmetcnp 13911 lgsval 14298 pw1nct 14634 peano4nninf 14637 |
Copyright terms: Public domain | W3C validator |