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 480 | . 2 |
3 | 2 | adantr 274 | 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: ad4antlr 486 nntr2 6367 phpm 6727 phplem4on 6729 fidifsnen 6732 fisbth 6745 fin0 6747 fin0or 6748 fiintim 6785 fisseneq 6788 djudom 6946 difinfsnlem 6952 enomnilem 6978 prmuloc 7342 cauappcvgprlemopl 7422 cauappcvgprlemdisj 7427 cauappcvgprlemladdfl 7431 caucvgprlemopl 7445 axcaucvglemcau 7674 xaddf 9582 xleaddadd 9625 ssfzo12bi 9957 rebtwn2zlemstep 9985 btwnzge0 10028 addmodlteq 10126 frecuzrdgg 10144 hashxp 10527 cjap 10633 caucvgre 10708 minmax 10956 xrminmax 10989 sumeq2 11083 fsumconst 11178 bezoutlemmain 11598 dfgcd2 11614 lcmgcdlem 11670 cnpnei 12299 cnntr 12305 txmetcnp 12598 peano4nninf 13096 nninfalllemn 13098 |
Copyright terms: Public domain | W3C validator |